{-# LANGUAGE OverloadedStrings    #-}
{-# LANGUAGE FlexibleContexts     #-}
{-# LANGUAGE TupleSections        #-}
{-# LANGUAGE EmptyDataDecls       #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# 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
  ) where

import Prelude hiding (error)
import           CoreSyn
import           Type (TyThing( AnId ))
import           Var
import           SrcLoc
import           Unify (tcUnifyTy)
import qualified TyCon   as TC
import qualified DataCon as DC
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               (catMaybes, isJust)
import           Control.Monad.State

import           Language.Haskell.Liquid.GHC.SpanStack
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 TC.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 = TargetInfo -> Config
forall t. HasConfig t => t -> Config
getConfig (TargetInfo -> Config) -> (CGEnv -> TargetInfo) -> CGEnv -> Config
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CGEnv -> TargetInfo
cgInfo

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

instance Monoid LConstraint where
  mempty :: LConstraint
mempty  = [[(Symbol, SpecType)]] -> LConstraint
LC []
  mappend :: LConstraint -> LConstraint -> LConstraint
mappend = LConstraint -> LConstraint -> LConstraint
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 [[(Symbol, SpecType)]]
-> [[(Symbol, SpecType)]] -> [[(Symbol, SpecType)]]
forall a. [a] -> [a] -> [a]
++ [[(Symbol, SpecType)]]
cs2)

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

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

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


subVar :: FixSubC -> Maybe Var
subVar :: FixSubC -> Maybe Var
subVar = Cinfo -> Maybe Var
ci_var (Cinfo -> Maybe Var) -> (FixSubC -> Cinfo) -> FixSubC -> Maybe Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FixSubC -> Cinfo
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 {}) = Tidy -> CGEnv -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k (SubC -> CGEnv
senv SubC
c)
                             Doc -> Doc -> Doc
$+$ (Doc
"||-" Doc -> Doc -> Doc
<+> [Doc] -> Doc
vcat [ Tidy -> SpecType -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k (SubC -> SpecType
lhs SubC
c)
                                                 , Doc
"<:"
                                                 , Tidy -> SpecType -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k (SubC -> SpecType
rhs SubC
c) ] )
  pprintTidy Tidy
k c :: SubC
c@(SubR {}) = Tidy -> CGEnv -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k (SubC -> CGEnv
senv SubC
c)
                             Doc -> Doc -> Doc
$+$ (Doc
"||-" Doc -> Doc -> Doc
<+> [Doc] -> Doc
vcat [ Tidy -> RReft -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k (SubC -> RReft
ref SubC
c)
                                                 , Doc -> Doc
parens (Tidy -> Oblig -> Doc
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
<+> Tidy -> SpecType -> 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 -> BindEnv
binds      :: !F.BindEnv                   -- ^ set of environment binders
  , CGInfo -> [Int]
ebinds     :: ![F.BindId]                  -- ^ existentials
  , CGInfo -> AnnInfo (Annot SpecType)
annotMap   :: !(AnnInfo (Annot SpecType))  -- ^ source-position annotation map
  , CGInfo -> HashMap Var (HoleInfo (CGInfo, CGEnv) SpecType)
holesMap   :: !(M.HashMap Var (HoleInfo (CGInfo, CGEnv) SpecType))    -- ^ information for ghc hole expressions
  , CGInfo -> TyConMap
tyConInfo  :: !TyConMap                    -- ^ information about type-constructors
  , CGInfo -> [(Var, [Int])]
specDecr   :: ![(Var, [Int])]              -- ^ ^ Lexicographic order of decreasing args (DEPRECATED) 
  , CGInfo -> HashMap TyCon SpecType
newTyEnv   :: !(M.HashMap TC.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 TC.TyCon)        -- ^ ? FIX THIS
  , CGInfo -> TCEmb TyCon
tyConEmbed :: !(F.TCEmb TC.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
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     <- CGInfo -> Bool
pruneRefs (CGInfo -> Bool)
-> StateT CGInfo Identity CGInfo -> StateT CGInfo Identity Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT CGInfo Identity CGInfo
forall s (m :: * -> *). MonadState s m => m s
get
  Templates
ts     <- CGInfo -> Templates
unsorted  (CGInfo -> Templates)
-> StateT CGInfo Identity CGInfo -> CG Templates
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT CGInfo Identity CGInfo
forall s (m :: * -> *). MonadState s m => m s
get
  Templates -> CG Templates
forall (m :: * -> *) a. Monad m => a -> m a
return (Templates -> CG Templates) -> Templates -> CG Templates
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 (HashSet Symbol -> HEnv)
-> ([Symbol] -> HashSet Symbol) -> [Symbol] -> HEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Symbol] -> HashSet Symbol
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 Symbol -> HashSet Symbol -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`S.member` HashSet Symbol
s

--------------------------------------------------------------------------------
-- | Helper Types: Invariants --------------------------------------------------
--------------------------------------------------------------------------------
data RInv = RInv { RInv -> [RSort]
_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
(Int -> RInv -> ShowS)
-> (RInv -> String) -> ([RInv] -> ShowS) -> Show RInv
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)]
ts = [(RTyCon, RInv)] -> RTyConInv
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k [v]
group [ (RTyCon
c, [RSort] -> SpecType -> Maybe Var -> RInv
RInv ([SpecType] -> [RSort]
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
_)) <- (Maybe Var, Located SpecType) -> (Maybe Var, SpecType)
forall a tv c r. (a, Located (RType tv c r)) -> (a, RType tv c r)
strip ((Maybe Var, Located SpecType) -> (Maybe Var, SpecType))
-> [(Maybe Var, Located SpecType)] -> [(Maybe Var, SpecType)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Maybe Var, Located SpecType)]
ts]
  where
    strip :: (a, Located (RType tv c r)) -> (a, RType tv c r)
strip = (Located (RType tv c r) -> RType tv c r)
-> (a, Located (RType tv c r)) -> (a, RType tv c r)
forall b c a. (b -> c) -> (a, b) -> (a, c)
mapSnd (([(RTVar c (RType tv c ()), r)], [PVar (RType tv c ())],
 RType tv c r)
-> RType tv c r
forall t1 t2 t3. (t1, t2, t3) -> t3
thrd3 (([(RTVar c (RType tv c ()), r)], [PVar (RType tv c ())],
  RType tv c r)
 -> RType tv c r)
-> (Located (RType tv c r)
    -> ([(RTVar c (RType tv c ()), r)], [PVar (RType tv c ())],
        RType tv c r))
-> Located (RType tv c r)
-> RType tv c r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RType tv c r
-> ([(RTVar c (RType tv c ()), r)], [PVar (RType tv c ())],
    RType tv c r)
forall tv c r.
RType tv c r
-> ([(RTVar c (RType tv c ()), r)], [PVar (RType tv c ())],
    RType tv c r)
bkUniv (RType tv c r
 -> ([(RTVar c (RType tv c ()), r)], [PVar (RType tv c ())],
     RType tv c r))
-> (Located (RType tv c r) -> RType tv c r)
-> Located (RType tv c r)
-> ([(RTVar c (RType tv c ()), r)], [PVar (RType tv c ())],
    RType tv c r)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located (RType tv c r) -> RType tv c r
forall a. Located a -> a
val)
    go :: [RType c tv r] -> [RType c tv ()]
go [RType c tv r]
ts | [RType c tv ()] -> Bool
forall tv r c. (Eq tv, Eq r, Eq c) => [RType c tv r] -> Bool
generic (RType c tv r -> RType c tv ()
forall c tv r. RType c tv r -> RType c tv ()
toRSort (RType c tv r -> RType c tv ())
-> [RType c tv r] -> [RType c tv ()]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RType c tv r]
ts) = []
          | Bool
otherwise                = RType c tv r -> RType c tv ()
forall c tv r. RType c tv r -> RType c tv ()
toRSort (RType c tv r -> RType c tv ())
-> [RType c tv r] -> [RType c tv ()]
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' = [RType c tv r] -> [RType c tv r]
forall a. Eq a => [a] -> [a]
L.nub [RType c tv r]
ts in
                 (RType c tv r -> Bool) -> [RType c tv r] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all RType c tv r -> Bool
forall c tv r. RType c tv r -> Bool
isRVar [RType c tv r]
ts' Bool -> Bool -> Bool
&& [RType c tv r] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [RType c tv r]
ts' Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [RType c tv r] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [RType c tv r]
ts

mkRTyConIAl :: [(a, F.Located SpecType)] -> RTyConInv
mkRTyConIAl :: [(a, Located SpecType)] -> RTyConInv
mkRTyConIAl    = [(Maybe Var, Located SpecType)] -> RTyConInv
mkRTyConInv ([(Maybe Var, Located SpecType)] -> RTyConInv)
-> ([(a, Located SpecType)] -> [(Maybe Var, Located SpecType)])
-> [(a, Located SpecType)]
-> RTyConInv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((a, Located SpecType) -> (Maybe Var, Located SpecType))
-> [(a, Located SpecType)] -> [(Maybe Var, Located SpecType)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Maybe Var
forall a. Maybe a
Nothing,) (Located SpecType -> (Maybe Var, Located SpecType))
-> ((a, Located SpecType) -> Located SpecType)
-> (a, Located SpecType)
-> (Maybe Var, Located SpecType)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a, Located SpecType) -> Located SpecType
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 -> (SpecType -> SpecType -> SpecType)
-> SpecType -> [SpecType] -> SpecType
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 RTyCon -> RTyConInv -> Maybe [RInv]
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup RTyCon
c RTyConInv
m of
      Maybe [RInv]
Nothing   -> Maybe [SpecType]
forall a. Maybe a
Nothing
      Just [RInv]
invs -> [SpecType] -> Maybe [SpecType]
forall a. a -> Maybe a
Just ([Maybe SpecType] -> [SpecType]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe SpecType] -> [SpecType]) -> [Maybe SpecType] -> [SpecType]
forall a b. (a -> b) -> a -> b
$ [SpecType] -> RInv -> Maybe SpecType
goodInvs [SpecType]
ts (RInv -> Maybe SpecType) -> [RInv] -> [Maybe SpecType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RInv]
invs)
lookupRInv SpecType
_ RTyConInv
_
  = Maybe [SpecType]
forall a. Maybe a
Nothing

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


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

addRInv :: RTyConInv -> (Var, SpecType) -> (Var, SpecType)
addRInv :: RTyConInv -> (Var, SpecType) -> (Var, SpecType)
addRInv RTyConInv
m (Var
x, SpecType
t)
  | Var
x Var -> [Var] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Var]
ids , Just [SpecType]
invs <- SpecType -> RTyConInv -> Maybe [SpecType]
lookupRInv (SpecType -> SpecType
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 ([RReft] -> RReft
forall a. Monoid a => [a] -> a
mconcat ([RReft] -> RReft) -> [RReft] -> RReft
forall a b. (a -> b) -> a -> b
$ [Maybe RReft] -> [RReft]
forall a. [Maybe a] -> [a]
catMaybes (SpecType -> Maybe RReft
forall c tv r. RType c tv r -> Maybe r
stripRTypeBase (SpecType -> Maybe RReft) -> [SpecType] -> [Maybe RReft]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SpecType]
invs)))
  | Bool
otherwise
  = (Var
x, SpecType
t)
   where
     ids :: [Var]
ids = [Var
id | RTyCon
tc <- RTyConInv -> [RTyCon]
forall k v. HashMap k v -> [k]
M.keys RTyConInv
m
               , DataCon
dc <- TyCon -> [DataCon]
TC.tyConDataCons (TyCon -> [DataCon]) -> TyCon -> [DataCon]
forall a b. (a -> b) -> a -> b
$ RTyCon -> TyCon
rtc_tc RTyCon
tc
               , AnId Var
id <- DataCon -> [TyThing]
DC.dataConImplicitTyThings DataCon
dc]
     res :: RType c tv r -> RType c tv r
res = RTypeRep c tv r -> RType c tv r
forall c tv r. RTypeRep c tv r -> RType c tv r
ty_res (RTypeRep c tv r -> RType c tv r)
-> (RType c tv r -> RTypeRep c tv r)
-> RType c tv r
-> RType c tv r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RType c tv r -> RTypeRep c tv r
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 (SpecType -> Symbol -> SpecType
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 (SpecType -> Symbol
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 RTyCon -> RTyCon -> Bool
forall a. Eq a => a -> a -> Bool
== RTyCon
ic Bool -> Bool -> Bool
&& [SpecType] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SpecType]
ts Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [SpecType] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SpecType]
its
  = RTyCon
-> [SpecType] -> [RTProp RTyCon RTyVar RReft] -> RReft -> SpecType
forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp RTyCon
c ((SpecType -> SpecType -> SpecType)
-> [SpecType] -> [SpecType] -> [SpecType]
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 RReft -> RReft -> RReft
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 RReft -> RReft -> RReft
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 RReft -> RReft -> RReft
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  = ([RInv] -> [RInv]) -> RTyConInv -> RTyConInv
forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
M.map ((RInv -> Bool) -> [RInv] -> [RInv]
forall a. (a -> Bool) -> [a] -> [a]
filter RInv -> Bool
f) (CGEnv -> RTyConInv
invs CGEnv
γ)
       , rinvs :: RTyConInv
rinvs = ([RInv] -> [RInv]) -> RTyConInv -> RTyConInv
forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
M.map ((RInv -> Bool) -> [RInv] -> [RInv]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (RInv -> Bool) -> RInv -> Bool
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 Var -> [Var] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` CoreBind -> [Var]
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)    = ([a], [Expr a]) -> [a]
forall a b. (a, b) -> a
fst (([a], [Expr a]) -> [a]) -> ([a], [Expr a]) -> [a]
forall a b. (a -> b) -> a -> b
$ [(a, Expr a)] -> ([a], [Expr a])
forall a b. [(a, b)] -> ([a], [b])
unzip [(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 = ([RInv] -> [RInv] -> [RInv]) -> RTyConInv -> RTyConInv -> RTyConInv
forall k v.
(Eq k, Hashable k) =>
(v -> v -> v) -> HashMap k v -> HashMap k v -> HashMap k v
M.unionWith [RInv] -> [RInv] -> [RInv]
forall a. [a] -> [a] -> [a]
(++) (CGEnv -> RTyConInv
invs CGEnv
γ) RTyConInv
is}
  where
    is :: RTyConInv
is  =  ([RInv] -> [RInv]) -> RTyConInv -> RTyConInv
forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
M.map ((RInv -> RInv) -> [RInv] -> [RInv]
forall a b. (a -> b) -> [a] -> [b]
map RInv -> RInv
f ([RInv] -> [RInv]) -> ([RInv] -> [RInv]) -> [RInv] -> [RInv]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (RInv -> Bool) -> [RInv] -> [RInv]
forall a. (a -> Bool) -> [a] -> [a]
filter (Maybe TCvSubst -> Bool
forall a. Maybe a -> Bool
isJust (Maybe TCvSubst -> Bool)
-> (RInv -> Maybe TCvSubst) -> RInv -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Var -> Type
varType Var
x Type -> Type -> Maybe TCvSubst
`tcUnifyTy`) (Type -> Maybe TCvSubst)
-> (RInv -> Type) -> RInv -> Maybe TCvSubst
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SpecType -> Type
forall r. ToTypeable r => RRType r -> Type
toType (SpecType -> Type) -> (RInv -> SpecType) -> RInv -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RInv -> SpecType
_rinv_type)) (CGEnv -> RTyConInv
rinvs CGEnv
γ)
    f :: RInv -> RInv
f RInv
i = RInv
i{_rinv_type :: SpecType
_rinv_type = SpecType -> SpecType
forall tv. RType RTyCon tv RReft -> RType RTyCon tv RReft
guard (SpecType -> SpecType) -> SpecType -> SpecType
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 (SizeFun -> Symbol -> Expr)
-> Maybe SizeFun -> Maybe (Symbol -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyConInfo -> Maybe SizeFun
sizeFunction (RTyCon -> TyConInfo
rtc_info RTyCon
c)
      = RTyCon
-> [RType RTyCon tv RReft]
-> [RTProp RTyCon tv RReft]
-> RReft
-> RType RTyCon tv RReft
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 (Reft -> Predicate -> RReft
forall r. r -> Predicate -> UReft r
MkUReft ((Symbol -> Expr) -> Reft -> Reft
ref Symbol -> Expr
f (Reft -> Reft) -> Reft -> Reft
forall a b. (a -> b) -> a -> b
$ RReft -> Reft
forall r. Reftable r => r -> Reft
F.toReft RReft
r) Predicate
forall a. Monoid a => a
mempty)
      | Bool
otherwise
      = RTyCon
-> [RType RTyCon tv RReft]
-> [RTProp RTyCon tv RReft]
-> RReft
-> RType RTyCon tv RReft
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 RReft
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 (Symbol -> Expr) -> Symbol -> Expr
forall a b. (a -> b) -> a -> b
$ Var -> Symbol
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)
       (Symbol -> Sort -> SEnv Sort -> SEnv Sort
forall a. Symbol -> a -> SEnv a -> SEnv a
F.insertSEnv Symbol
x Sort
t      SEnv Sort
env)
       (Symbol -> Int -> SEnv Int -> SEnv Int
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 = (FEnv -> ((Symbol, Sort), Int) -> FEnv)
-> FEnv -> [((Symbol, Sort), Int)] -> FEnv
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 SEnv Int
forall a. SEnv a
ienv0
  where
    benv0 :: IBindEnv
benv0    = IBindEnv
F.emptyIBindEnv
    env0 :: SEnv Sort
env0     = [(Symbol, Sort)] -> SEnv Sort
forall a. [(Symbol, a)] -> SEnv a
F.fromListSEnv ([(Symbol, Sort)]
wiredSortedSyms [(Symbol, Sort)] -> [(Symbol, Sort)] -> [(Symbol, Sort)]
forall a. [a] -> [a] -> [a]
++ [(Symbol, Sort)]
xts)
    ienv0 :: SEnv a
ienv0    = SEnv a
forall a. SEnv a
F.emptySEnv

--------------------------------------------------------------------------------
-- | Forcing Strictness --------------------------------------------------------
--------------------------------------------------------------------------------
instance NFData RInv where
  rnf :: RInv -> ()
rnf (RInv [RSort]
x SpecType
y Maybe Var
z) = [RSort] -> ()
forall a. NFData a => a -> ()
rnf [RSort]
x () -> () -> ()
`seq` SpecType -> ()
forall a. NFData a => a -> ()
rnf SpecType
y () -> () -> ()
`seq` Maybe Var -> ()
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 SpanStack -> () -> ()
`seq` {- rnf x2 `seq` -} SEnv Var -> Any -> Any
seq SEnv Var
x3
         (Any -> Any) -> () -> ()
`seq` SEnv Sort -> ()
forall a. NFData a => a -> ()
rnf SEnv Sort
x5
         () -> () -> ()
`seq` FEnv -> ()
forall a. NFData a => a -> ()
rnf FEnv
x55
         () -> () -> ()
`seq` HashSet Var -> ()
forall a. NFData a => a -> ()
rnf HashSet Var
x6
         () -> () -> ()
`seq` RTyConInv
x7
         RTyConInv -> () -> ()
`seq` RTyConInv -> ()
forall a. NFData a => a -> ()
rnf RTyConInv
x8
         () -> () -> ()
`seq` RTyConInv -> ()
forall a. NFData a => a -> ()
rnf RTyConInv
x9
         () -> () -> ()
`seq` TCEmb TyCon -> ()
forall a. NFData a => a -> ()
rnf TCEmb TyCon
x10
         () -> () -> ()
`seq` SEnv Sort -> ()
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) = IBindEnv -> ()
forall a. NFData a => a -> ()
rnf IBindEnv
x1 () -> () -> ()
`seq` SEnv Sort -> ()
forall a. NFData a => a -> ()
rnf SEnv Sort
x2 () -> () -> ()
`seq` SEnv Int -> ()
forall a. NFData a => a -> ()
rnf SEnv Int
x3

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

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

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