{-# 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.UX.Config

import           Language.Haskell.Liquid.Types.Errors
import           Language.Haskell.Liquid.Types.RefType
import           Language.Haskell.Liquid.Types.RType
import           Language.Haskell.Liquid.Types.RTypeOp
import           Language.Haskell.Liquid.Types.Specs
import           Language.Haskell.Liquid.Types.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 -> 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 = 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

newtype 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

getLocation :: CGEnv -> SrcSpan
getLocation :: CGEnv -> SrcSpan
getLocation = SpanStack -> SrcSpan
srcSpan (SpanStack -> SrcSpan) -> (CGEnv -> SpanStack) -> CGEnv -> 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 -> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
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 (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 {} =
    Doc
"The environment:"
    Doc -> Doc -> Doc
$+$
    Doc
""
    Doc -> Doc -> Doc
$+$
    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
"Location: " Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Tidy -> SrcSpan -> Doc
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 [ 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 {} =
    Doc
"The environment:"
    Doc -> Doc -> Doc
$+$
    Doc
""
    Doc -> Doc -> Doc
$+$
    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
"Location: " Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Tidy -> SrcSpan -> Doc
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 [ Tidy -> UReftBV Symbol Symbol (ReftBV Symbol Symbol) -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k (SubC -> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
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 -> FixBindEnv
binds         :: !FixBindEnv                         -- ^ set of environment binders
  , CGInfo -> LocalRewritesEnv
localRewrites :: !F.LocalRewritesEnv                 -- ^ set of local rewrites
  , 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
  , CGInfo
-> HashMap (Var, SrcSpan) (HoleInfo (CGInfo, CGEnv) SpecType)
hsHoles       :: !(M.HashMap (Var, SrcSpan) (HoleInfo (CGInfo, CGEnv) SpecType)) -- Information about holes in terms
  , CGInfo -> HashMap Var (Var, SrcSpan)
hsANFHoles    :: !(M.HashMap Var  (Var, SrcSpan))
  , CGInfo -> HashMap (Var, SrcSpan) [(Var, CoreExpr, SpecType)]
hsHolesExprs  :: !(M.HashMap (Var, SrcSpan)  [(Var, CoreExpr, SpecType)])
  }


getTemplates :: CG F.Templates
getTemplates :: CG Templates
getTemplates = do
  fg    <- (CGInfo -> Bool) -> StateT CGInfo Identity Bool
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CGInfo -> Bool
pruneRefs
  ts    <- gets unsorted
  return $ if fg then F.anything else 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. 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. Hashable a => a -> HashSet a -> Bool
`S.member` HashSet Symbol
s

--------------------------------------------------------------------------------
-- | Helper Types: Invariants --------------------------------------------------
--------------------------------------------------------------------------------
data RInv = RInv { RInv -> [RRType NoReft]
_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
$cshowsPrec :: Int -> RInv -> ShowS
showsPrec :: Int -> RInv -> ShowS
$cshow :: RInv -> String
show :: RInv -> String
$cshowList :: [RInv] -> ShowS
showList :: [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 = [(RTyCon, RInv)] -> RTyConInv
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k [v]
group [ (RTyCon
c, [RRType NoReft] -> SpecType -> Maybe Var -> RInv
RInv ([SpecType] -> [RRType NoReft]
forall {tv} {c} {r}.
(Eq tv, Eq c) =>
[RTypeBV Symbol Symbol c tv r]
-> [RTypeBV Symbol Symbol c tv NoReft]
go [SpecType]
ts) SpecType
t Maybe Var
v) | (Maybe Var
v, t :: SpecType
t@(RApp RTyCon
c [SpecType]
ts [RTPropBV
   Symbol
   Symbol
   RTyCon
   RTyVar
   (UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
_ UReftBV Symbol Symbol (ReftBV Symbol Symbol)
_)) <- (Maybe Var, Located SpecType) -> (Maybe Var, SpecType)
forall {b} {v} {tv} {c} {r}.
(Maybe Var, Located (RTypeBV b v tv c r))
-> (Maybe Var, RTypeBV b v 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)]
tss]
  where
    strip :: (Maybe Var, Located (RTypeBV b v tv c r))
-> (Maybe Var, RTypeBV b v tv c r)
strip = (Located (RTypeBV b v tv c r) -> RTypeBV b v tv c r)
-> (Maybe Var, Located (RTypeBV b v tv c r))
-> (Maybe Var, RTypeBV b v tv c r)
forall a b. (a -> b) -> (Maybe Var, a) -> (Maybe Var, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (([(RTVar c (RTypeBV b v tv c (NoReftB b)), r)],
 [PVarBV b v (RTypeBV b v tv c (NoReftB b))], RTypeBV b v tv c r)
-> RTypeBV b v tv c r
forall t1 t2 t3. (t1, t2, t3) -> t3
thrd3 (([(RTVar c (RTypeBV b v tv c (NoReftB b)), r)],
  [PVarBV b v (RTypeBV b v tv c (NoReftB b))], RTypeBV b v tv c r)
 -> RTypeBV b v tv c r)
-> (Located (RTypeBV b v tv c r)
    -> ([(RTVar c (RTypeBV b v tv c (NoReftB b)), r)],
        [PVarBV b v (RTypeBV b v tv c (NoReftB b))], RTypeBV b v tv c r))
-> Located (RTypeBV b v tv c r)
-> RTypeBV b v tv c r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTypeBV b v tv c r
-> ([(RTVar c (RTypeBV b v tv c (NoReftB b)), r)],
    [PVarBV b v (RTypeBV b v tv c (NoReftB b))], RTypeBV b v tv c r)
forall b v tv c r.
RTypeBV b v tv c r
-> ([(RTVar c (RTypeBV b v tv c (NoReftB b)), r)],
    [PVarBV b v (RTypeBV b v tv c (NoReftB b))], RTypeBV b v tv c r)
bkUniv (RTypeBV b v tv c r
 -> ([(RTVar c (RTypeBV b v tv c (NoReftB b)), r)],
     [PVarBV b v (RTypeBV b v tv c (NoReftB b))], RTypeBV b v tv c r))
-> (Located (RTypeBV b v tv c r) -> RTypeBV b v tv c r)
-> Located (RTypeBV b v tv c r)
-> ([(RTVar c (RTypeBV b v tv c (NoReftB b)), r)],
    [PVarBV b v (RTypeBV b v tv c (NoReftB b))], RTypeBV b v tv c r)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located (RTypeBV b v tv c r) -> RTypeBV b v tv c r
forall a. Located a -> a
val)
    go :: [RTypeBV Symbol Symbol c tv r]
-> [RTypeBV Symbol Symbol c tv NoReft]
go [RTypeBV Symbol Symbol c tv r]
ts | [RTypeBV Symbol Symbol c tv NoReft] -> Bool
forall {tv} {c} {r}.
(Eq tv, Eq c, Eq r) =>
[RTypeBV Symbol Symbol c tv r] -> Bool
generic (RTypeBV Symbol Symbol c tv r -> RTypeBV Symbol Symbol c tv NoReft
forall b v c tv r.
Binder b =>
RTypeBV b v c tv r -> RTypeBV b v c tv (NoReftB b)
toRSort (RTypeBV Symbol Symbol c tv r -> RTypeBV Symbol Symbol c tv NoReft)
-> [RTypeBV Symbol Symbol c tv r]
-> [RTypeBV Symbol Symbol c tv NoReft]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RTypeBV Symbol Symbol c tv r]
ts) = []
          | Bool
otherwise                = RTypeBV Symbol Symbol c tv r -> RTypeBV Symbol Symbol c tv NoReft
forall b v c tv r.
Binder b =>
RTypeBV b v c tv r -> RTypeBV b v c tv (NoReftB b)
toRSort (RTypeBV Symbol Symbol c tv r -> RTypeBV Symbol Symbol c tv NoReft)
-> [RTypeBV Symbol Symbol c tv r]
-> [RTypeBV Symbol Symbol c tv NoReft]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RTypeBV Symbol Symbol c tv r]
ts

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

mkRTyConIAl :: [(a, F.Located SpecType)] -> RTyConInv
mkRTyConIAl :: forall a. [(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 a b. (a -> b) -> [a] -> [b]
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 b a. (b -> a -> b) -> b -> [a] -> b
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 [RTPropBV
   Symbol
   Symbol
   RTyCon
   RTyVar
   (UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
_ UReftBV Symbol Symbol (ReftBV Symbol Symbol)
_) RTyConInv
m
  = case RTyCon -> RTyConInv -> Maybe [RInv]
forall k v. 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 ((RInv -> Maybe SpecType) -> [RInv] -> [SpecType]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe ([SpecType] -> RInv -> Maybe SpecType
goodInvs [SpecType]
ts) [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 [RRType NoReft]
ts' SpecType
t Maybe Var
_)
  | [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ((RRType NoReft -> RRType NoReft -> Bool)
-> [RRType NoReft] -> [RRType NoReft] -> [Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith RRType NoReft -> RRType NoReft -> Bool
invMatchesTarget [RRType NoReft]
ts' (SpecType -> RRType NoReft
forall b v c tv r.
Binder b =>
RTypeBV b v c tv r -> RTypeBV b v c tv (NoReftB b)
toRSort (SpecType -> RRType NoReft) -> [SpecType] -> [RRType NoReft]
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


-- | Check that the target type arg is an instance of the invariant's type arg.
-- Uses one-directional matching (tcMatchTy) so that a type variable in the
-- target does NOT unify with a structured invariant arg. This prevents e.g.
-- an invariant for [Diff [a]] from being applied to a plain [a] binder.
invMatchesTarget :: RSort -> RSort -> Bool
invMatchesTarget :: RRType NoReft -> RRType NoReft -> Bool
invMatchesTarget RRType NoReft
inv RRType NoReft
tgt = Maybe Subst -> Bool
forall a. Maybe a -> Bool
isJust (Maybe Subst -> Bool) -> Maybe Subst -> Bool
forall a b. (a -> b) -> a -> b
$ HasDebugCallStack => Type -> Type -> Maybe Subst
Type -> Type -> Maybe Subst
tcMatchTy (Bool -> RRType NoReft -> Type
forall r. ToTypeable r => Bool -> RRType r -> Type
toType Bool
False RRType NoReft
inv) (Bool -> RRType NoReft -> Type
forall r. ToTypeable r => Bool -> RRType r -> Type
toType Bool
False RRType NoReft
tgt)

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 a. Eq a => a -> [a] -> 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 {b} {v} {c} {tv} {r}.
RTypeBV b v c tv r -> RTypeBV b v c tv r
res SpecType
t) RTyConInv
m
  = (Var
x, SpecType
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol) -> SpecType
addInvCond SpecType
t ([UReftBV Symbol Symbol (ReftBV Symbol Symbol)]
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
forall a. Monoid a => [a] -> a
mconcat ([UReftBV Symbol Symbol (ReftBV Symbol Symbol)]
 -> UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> [UReftBV Symbol Symbol (ReftBV Symbol Symbol)]
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
forall a b. (a -> b) -> a -> b
$ (SpecType -> Maybe (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
-> [SpecType] -> [UReftBV Symbol Symbol (ReftBV Symbol Symbol)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe SpecType -> Maybe (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
forall b v c tv r. RTypeBV b v c tv r -> Maybe r
stripRTypeBase [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]
Ghc.tyConDataCons (TyCon -> [DataCon]) -> TyCon -> [DataCon]
forall a b. (a -> b) -> a -> b
$ RTyCon -> TyCon
rtc_tc RTyCon
tc
               , AnId Var
id' <- DataCon -> [TyThing]
Ghc.dataConImplicitTyThings DataCon
dc]
     res :: RTypeBV b v c tv r -> RTypeBV b v c tv r
res = RTypeRepBV b v c tv r -> RTypeBV b v c tv r
forall b v c tv r. RTypeRepBV b v c tv r -> RTypeBV b v c tv r
ty_res (RTypeRepBV b v c tv r -> RTypeBV b v c tv r)
-> (RTypeBV b v c tv r -> RTypeRepBV b v c tv r)
-> RTypeBV b v c tv r
-> RTypeBV b v c tv r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTypeBV b v c tv r -> RTypeRepBV b v c tv r
forall b v c tv r. RTypeBV b v c tv r -> RTypeRepBV b v 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, IsReft (f (ReftBV Symbol Symbol)), Functor f,
 Subable (f (ReftBV Symbol Symbol)),
 Variable (f (ReftBV Symbol Symbol))
 ~ Variable (ReftBV Symbol Symbol),
 ReftBind (f (ReftBV Symbol Symbol))
 ~ ReftBind (ReftBV Symbol Symbol)) =>
RType c tv (f (ReftBV Symbol Symbol))
-> Symbol -> RType c tv (f (ReftBV Symbol Symbol))
shiftVV SpecType
t2 (SpecType -> ReftBind (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
forall r b v c tv.
(ToReft r, Binder (ReftBind r)) =>
RTypeBV b v c tv r -> ReftBind r
rTypeValueVar SpecType
t1))

conjoinInvariant :: SpecType -> SpecType -> SpecType
conjoinInvariant :: SpecType -> SpecType -> SpecType
conjoinInvariant (RApp RTyCon
c [SpecType]
ts [RTPropBV
   Symbol
   Symbol
   RTyCon
   RTyVar
   (UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
rs UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r) (RApp RTyCon
ic [SpecType]
its [RTPropBV
   Symbol
   Symbol
   RTyCon
   RTyVar
   (UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
_ UReftBV Symbol Symbol (ReftBV Symbol Symbol)
ir)
  | RTyCon
c RTyCon -> RTyCon -> Bool
forall a. Eq a => a -> a -> Bool
== RTyCon
ic Bool -> Bool -> Bool
&& [SpecType] -> Int
forall a. [a] -> 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 a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SpecType]
its
  = RTyCon
-> [SpecType]
-> [RTPropBV
      Symbol
      Symbol
      RTyCon
      RTyVar
      (UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> SpecType
forall b v c tv r.
c
-> [RTypeBV b v c tv r]
-> [RTPropBV b v c tv r]
-> r
-> RTypeBV b v c tv r
RApp RTyCon
c ((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) [RTPropBV
   Symbol
   Symbol
   RTyCon
   RTyVar
   (UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
rs (UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
forall r. Meet r => r -> r -> r
`meet` UReftBV Symbol Symbol (ReftBV Symbol Symbol)
ir)

conjoinInvariant t :: SpecType
t@(RApp RTyCon
_ [SpecType]
_ [RTPropBV
   Symbol
   Symbol
   RTyCon
   RTyVar
   (UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
_ UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r) (RVar RTyVar
_ UReftBV Symbol Symbol (ReftBV Symbol Symbol)
ir)
  = SpecType
t { rt_reft = r `meet` ir }

conjoinInvariant t :: SpecType
t@(RVar RTyVar
_ UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r) (RVar RTyVar
_ UReftBV Symbol Symbol (ReftBV Symbol Symbol)
ir)
  = SpecType
t { rt_reft = r `meet` ir }

conjoinInvariant SpecType
t SpecType
_
  = SpecType
t

removeInvariant  :: CGEnv -> CoreBind -> (CGEnv, RTyConInv)
removeInvariant :: CGEnv -> CoreBind -> (CGEnv, RTyConInv)
removeInvariant CGEnv
γ CoreBind
cbs
  = (CGEnv
γ { invs  = M.map (filter f) (invs γ)
       , rinvs = M.map (filter (not . f)) (invs γ)}
    , 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 a. Eq a => a -> [a] -> 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) -> [(a, Expr a)] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (a, Expr a) -> a
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 = is}

makeRecInvariants :: CGEnv -> [Var] -> CGEnv
makeRecInvariants :: CGEnv -> [Var] -> CGEnv
makeRecInvariants CGEnv
γ [Var
x] = CGEnv
γ {invs = M.unionWith (++) (invs γ) 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
g ([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 Subst -> Bool
forall a. Maybe a -> Bool
isJust (Maybe Subst -> Bool) -> (RInv -> Maybe Subst) -> RInv -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Var -> Type
varType Var
x Type -> Type -> Maybe Subst
`tcUnifyTy`) (Type -> Maybe Subst) -> (RInv -> Type) -> RInv -> Maybe Subst
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> SpecType -> Type
forall r. ToTypeable r => Bool -> RRType r -> Type
toType Bool
False (SpecType -> Type) -> (RInv -> SpecType) -> RInv -> Type
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 = guard' $ _rinv_type i}

    guard' :: RTypeBV
  b v RTyCon tv (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> RTypeBV
     b v RTyCon tv (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
guard' (RApp RTyCon
c [RTypeBV
   b v RTyCon tv (UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
ts [RTPropBV
   b v RTyCon tv (UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
rs UReftBV Symbol Symbol (ReftBV Symbol Symbol)
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
-> [RTypeBV
      b v RTyCon tv (UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
-> [RTPropBV
      b v RTyCon tv (UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> RTypeBV
     b v RTyCon tv (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
forall b v c tv r.
c
-> [RTypeBV b v c tv r]
-> [RTPropBV b v c tv r]
-> r
-> RTypeBV b v c tv r
RApp RTyCon
c [RTypeBV
   b v RTyCon tv (UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
ts [RTPropBV
   b v RTyCon tv (UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
rs (ReftBV Symbol Symbol
-> PredicateBV Symbol Symbol
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
forall b v r. r -> PredicateBV b v -> UReftBV b v r
MkUReft ((Symbol -> Expr) -> ReftBV Symbol Symbol -> ReftBV Symbol Symbol
forall {v}.
(Symbol -> ExprBV Symbol v) -> ReftBV Symbol v -> ReftBV Symbol v
ref Symbol -> Expr
f (ReftBV Symbol Symbol -> ReftBV Symbol Symbol)
-> ReftBV Symbol Symbol -> ReftBV Symbol Symbol
forall a b. (a -> b) -> a -> b
$ UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> ReftBV
     (ReftBind (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
     (ReftVar (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
forall r. ToReft r => r -> ReftBV (ReftBind r) (ReftVar r)
toReft UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r) PredicateBV Symbol Symbol
forall a. Monoid a => a
mempty)
      | Bool
otherwise
      = RTyCon
-> [RTypeBV
      b v RTyCon tv (UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
-> [RTPropBV
      b v RTyCon tv (UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> RTypeBV
     b v RTyCon tv (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
forall b v c tv r.
c
-> [RTypeBV b v c tv r]
-> [RTPropBV b v c tv r]
-> r
-> RTypeBV b v c tv r
RApp RTyCon
c [RTypeBV
   b v RTyCon tv (UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
ts [RTPropBV
   b v RTyCon tv (UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
rs UReftBV Symbol Symbol (ReftBV Symbol Symbol)
forall a. Monoid a => a
mempty
    guard' RTypeBV
  b v RTyCon tv (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
t
      = RTypeBV
  b v RTyCon tv (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
t

    ref :: (Symbol -> ExprBV Symbol v) -> ReftBV Symbol v -> ReftBV Symbol v
ref Symbol -> ExprBV Symbol v
f (F.Reft(Symbol
v, ExprBV Symbol v
rr))
      = (Symbol, ExprBV Symbol v) -> ReftBV Symbol v
forall b v. (b, ExprBV b v) -> ReftBV b v
F.Reft (Symbol
v, ExprBV Symbol v -> ExprBV Symbol v -> ExprBV Symbol v
forall b v. ExprBV b v -> ExprBV b v -> ExprBV b v
F.PImp (Brel -> ExprBV Symbol v -> ExprBV Symbol v -> ExprBV Symbol v
forall b v. Brel -> ExprBV b v -> ExprBV b v -> ExprBV b v
F.PAtom Brel
F.Lt (Symbol -> ExprBV Symbol v
f Symbol
v) (Symbol -> ExprBV Symbol v
f (Symbol -> ExprBV Symbol v) -> Symbol -> ExprBV Symbol v
forall a b. (a -> b) -> a -> b
$ Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
x)) ExprBV Symbol v
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 b a. Hashable b => b -> a -> SEnvB b a -> SEnvB b a
F.insertSEnv Symbol
x Sort
t      SEnv Sort
env)
       (Symbol -> Int -> SEnv Int -> SEnv Int
forall b a. Hashable b => b -> a -> SEnvB b a -> SEnvB b 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 b a. (b -> a -> b) -> b -> [a] -> b
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 {b} {a}. SEnvB b a
ienv0
  where
    benv0 :: IBindEnv
benv0    = IBindEnv
F.emptyIBindEnv
    env0 :: SEnv Sort
env0     = [(Symbol, Sort)] -> SEnv Sort
forall b a. Hashable b => [(b, a)] -> SEnvB b a
F.fromListSEnv ([(Symbol, Sort)]
wiredSortedSyms [(Symbol, Sort)] -> [(Symbol, Sort)] -> [(Symbol, Sort)]
forall a. [a] -> [a] -> [a]
++ [(Symbol, Sort)]
xts)
    ienv0 :: SEnvB b a
ienv0    = SEnvB b a
forall {b} {a}. SEnvB b a
F.emptySEnv

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

instance NFData CGEnv where
  rnf :: CGEnv -> ()
rnf (CGE SpanStack
x1 REnv
_ 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 -> () -> ()
forall a b. a -> b -> b
`seq` SEnv Sort -> ()
forall a. NFData a => a -> ()
rnf SEnv Sort
x5
         () -> () -> ()
forall a b. a -> b -> b
`seq` FEnv -> ()
forall a. NFData a => a -> ()
rnf FEnv
x55
         () -> () -> ()
forall a b. a -> b -> b
`seq` HashSet Var -> ()
forall a. NFData a => a -> ()
rnf HashSet Var
x6
         () -> () -> ()
forall a b. a -> b -> b
`seq` RTyConInv
x7
         RTyConInv -> () -> ()
forall a b. a -> b -> b
`seq` RTyConInv -> ()
forall a. NFData a => a -> ()
rnf RTyConInv
x8
         () -> () -> ()
forall a b. a -> b -> b
`seq` RTyConInv -> ()
forall a. NFData a => a -> ()
rnf RTyConInv
x9
         () -> () -> ()
forall a b. a -> b -> b
`seq` TCEmb TyCon -> ()
forall a. NFData a => a -> ()
rnf TCEmb TyCon
x10
         () -> () -> ()
forall a b. a -> b -> b
`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 () -> () -> ()
forall a b. a -> b -> b
`seq` SEnv Sort -> ()
forall a. NFData a => a -> ()
rnf SEnv Sort
x2 () -> () -> ()
forall a b. a -> b -> b
`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 () -> () -> ()
forall a b. a -> b -> b
`seq` SpecType -> ()
forall a. NFData a => a -> ()
rnf SpecType
x2 () -> () -> ()
forall a b. a -> b -> b
`seq` SpecType -> ()
forall a. NFData a => a -> ()
rnf SpecType
x3
  rnf (SubR CGEnv
x1 Oblig
_ UReftBV Symbol Symbol (ReftBV Symbol Symbol)
x2)
    = CGEnv -> ()
forall a. NFData a => a -> ()
rnf CGEnv
x1 () -> () -> ()
forall a b. a -> b -> b
`seq` UReftBV Symbol Symbol (ReftBV Symbol Symbol) -> ()
forall a. NFData a => a -> ()
rnf UReftBV Symbol Symbol (ReftBV Symbol Symbol)
x2

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