{-# LANGUAGE ScopedTypeVariables       #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE FlexibleContexts          #-}
{-# LANGUAGE FlexibleInstances         #-}
{-# LANGUAGE TupleSections             #-}
{-# LANGUAGE PatternGuards             #-}
{-# LANGUAGE MultiParamTypeClasses     #-}
{-# LANGUAGE OverloadedStrings         #-}
{-# LANGUAGE ImplicitParams            #-}
{-# LANGUAGE NamedFieldPuns            #-}
{-# LANGUAGE TypeOperators             #-}

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

-- | This module defines the representation of Subtyping and WF Constraints,
--   and the code for syntax-directed constraint generation.

module Language.Haskell.Liquid.Constraint.Generate ( generateConstraints, caseEnv, consE ) where

import           Prelude                                       hiding (error)
import           GHC.Stack ( CallStack )
import           Liquid.GHC.API               as Ghc hiding ( panic
                                                            , (<+>)
                                                            , text
                                                            , vcat
                                                            )
import qualified Language.Haskell.Liquid.GHC.Resugar           as Rs
import qualified Language.Haskell.Liquid.GHC.SpanStack         as Sp
import qualified Language.Haskell.Liquid.GHC.Misc              as GM -- ( isInternal, collectArguments, tickSrcSpan, showPpr )
import Text.PrettyPrint.HughesPJ ( text )
import           Control.Monad ( foldM, forM, forM_, when, void, unless)
import           Control.Monad.State
import           Data.Bifunctor                                (first)
import           Data.Maybe                                    (fromMaybe, isJust, mapMaybe)
import           Data.Either.Extra                             (eitherToMaybe)
import qualified Data.HashMap.Strict                           as M
import qualified Data.HashSet                                  as S
import qualified Data.List                                     as L
import qualified Data.Foldable                                 as F
import qualified Data.Functor.Identity
import Language.Fixpoint.Misc (errorP, safeZip )
import           Language.Fixpoint.Types.Visitor
import qualified Language.Fixpoint.Types                       as F
import qualified Language.Fixpoint.Types.Visitor               as F
import           Language.Haskell.Liquid.Constraint.Fresh ( addKuts, freshTyType, trueTy )
import           Language.Haskell.Liquid.Constraint.Init ( initEnv, initCGI )
import           Language.Haskell.Liquid.Constraint.Env
import           Language.Haskell.Liquid.Constraint.Monad
import Language.Haskell.Liquid.Constraint.Split ( splitC, splitW )
import           Language.Haskell.Liquid.Constraint.Relational (consAssmRel, consRelTop)
import           Language.Haskell.Liquid.Types.Dictionaries
import           Language.Haskell.Liquid.Types.Errors
import           Language.Haskell.Liquid.Types.Fresh
import           Language.Haskell.Liquid.Types.Literals
import           Language.Haskell.Liquid.Types.Names
import           Language.Haskell.Liquid.Types.PredType
import           Language.Haskell.Liquid.Types.RType
import           Language.Haskell.Liquid.Types.RTypeOp
import           Language.Haskell.Liquid.Types.RefType
import           Language.Haskell.Liquid.Types.Specs
import           Language.Haskell.Liquid.Types.Types hiding (binds)
import           Language.Haskell.Liquid.Constraint.Types
import           Language.Haskell.Liquid.Constraint.Constraint ( addConstraints )
import           Language.Haskell.Liquid.Constraint.Template
import           Language.Haskell.Liquid.Constraint.Termination
import           Language.Haskell.Liquid.Constraint.RewriteCase
import           Language.Haskell.Liquid.Transforms.CoreToLogic (weakenResult, runToLogic, coreToLogic)
import           Language.Haskell.Liquid.Bare.DataType (dataConMap, makeDataConChecker)
import Language.Haskell.Liquid.UX.Config
    ( HasConfig(getConfig),
      Config(typeclass, checkDerived, extensionality,
             nopolyinfer, dependantCase, rankNTypes, warnOnTermHoles),
      patternFlag,
      higherOrderFlag, warnOnTermHoles )
import qualified GHC.Data.Strict as Strict

-- Note [Term holes]
--
-- The term-hole implementation in this module is a small, opt-in pipeline that
-- is only active when @warnOnTermHoles@ is enabled.
--
-- The thesis motivating this feature chose constraint generation as the hook for
-- hole support because this is the first phase where LiquidHaskell already knows
-- the refined types and local environment that make a warning actionable. An
-- earlier location-based approach would have been more modular, but the needed
-- query from source locations back into constraint generation was not feasible.
--
-- The implementation also uses a stable hole naming convention, recognized by
-- 'isVarHole', instead of depending on GHC surface syntax alone. This keeps the
-- matching logic local to Core while reducing the amount of desugaring detail we
-- have to reconstruct.
--
-- 1. We detect direct occurrences of a typed hole with 'detectTypedHole', which
--    peels away ticks via 'stripTicks', recovers the hole source span with
--    'lastTick', and recognizes @hole@ binders with 'isVarHole'. We need this
--    normalization-aware detection because holes can appear under GHC-introduced
--    @App@ and @Tick@ nodes, and the warning should still point at the original
--    source span.
--
-- 2. We remember hole-shaped let-bindings in 'consCB''s local @checkLetHole@
--    helper. That helper records which ANF binder names a hole by calling
--    'linkANFToHole'. This step is needed because LiquidHaskell's ANF
--    normalization can float a hole into a fresh @let@ binder, and later useful
--    constraints may mention only that ANF name instead of the original hole.
--
-- 3. We record the type and environment of each direct hole occurrence while
--    generating constraints. In checking mode, 'cconsE''s local @maybeAddHole@
--    stores the expected type with 'addHole'. In synthesis mode, 'consE''s
--    local @synthesizeWithHole@ first synthesizes the application's type and
--    then stores that synthesized type with 'addHole'. We need both sites:
--    checking gives the expected type when one is available, while synthesis
--    covers cases like applications where checking alone would only report an
--    uninformative base type for the hole.
--
-- 4. We attach ANF expressions that participate in a hole by running
--    'checkANFHoleInExpr' from 'cconsE' and from the application case of
--    'consE'. That helper walks the expression with 'collectVars', resolves any
--    binder previously linked by 'linkANFToHole' through 'isANFInHole', and
--    saves the expression/type pair with 'addHoleANF'. This is what recovers the
--    surrounding refined constraints that users actually need when the hole sits
--    inside a larger normalized expression.
--
-- 5. After constraint generation finishes, 'consAct' calls
--    'emitConsolidatedHoleWarnings'. It merges the stored hole metadata with the
--    collected ANF expressions and emits one 'ErrHole' warning per hole, using
--    the environment captured by 'addHole' so the warning reports the local
--    typing context that was in scope at the hole. Delaying emission until the
--    end is important: only then do we have the direct hole information, the ANF
--    links, and the extra constraints together in one place.
--
-- Term holes were developed during the Master's thesis
--
-- Enhancing Proof Development in LiquidHaskell: Implementation and Evaluation of Typed Holes
-- MATHEUS DE SOUSA BERNARDO
-- Chalmers University of Technology, 2025
--
-- https://odr.chalmers.se/server/api/core/bitstreams/640ee29b-b13a-44d5-9e20-200a91a11021/content

--------------------------------------------------------------------------------
-- | Constraint Generation: Toplevel -------------------------------------------
--------------------------------------------------------------------------------
generateConstraints      :: TargetInfo -> CGInfo
--------------------------------------------------------------------------------
generateConstraints :: TargetInfo -> CGInfo
generateConstraints TargetInfo
info = {-# SCC "ConsGen" #-} State CGInfo () -> CGInfo -> CGInfo
forall s a. State s a -> s -> s
execState State CGInfo ()
act (CGInfo -> CGInfo) -> CGInfo -> CGInfo
forall a b. (a -> b) -> a -> b
$ Config -> TargetInfo -> CGInfo
initCGI Config
cfg TargetInfo
info
  where
    act :: State CGInfo ()
act                  = do { γ <- TargetInfo -> CG CGEnv
initEnv TargetInfo
info; consAct γ cfg info }
    cfg :: Config
cfg                  = TargetInfo -> Config
forall t. HasConfig t => t -> Config
getConfig   TargetInfo
info

consAct :: CGEnv -> Config -> TargetInfo -> CG ()
consAct :: CGEnv -> Config -> TargetInfo -> State CGInfo ()
consAct CGEnv
γ Config
cfg TargetInfo
info = do
  let sSpc :: GhcSpecSig
sSpc = TargetSpec -> GhcSpecSig
gsSig (TargetSpec -> GhcSpecSig)
-> (TargetInfo -> TargetSpec) -> TargetInfo -> GhcSpecSig
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TargetInfo -> TargetSpec
giSpec (TargetInfo -> GhcSpecSig) -> TargetInfo -> GhcSpecSig
forall a b. (a -> b) -> a -> b
$ TargetInfo
info
  let gSrc :: TargetSrc
gSrc = TargetInfo -> TargetSrc
giSrc TargetInfo
info
  γ' <- (CGEnv -> Bind Var -> CG CGEnv) -> CGEnv -> [Bind Var] -> CG CGEnv
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (Config -> TargetInfo -> CGEnv -> Bind Var -> CG CGEnv
consCBTop Config
cfg TargetInfo
info) CGEnv
γ (TargetSrc -> [Bind Var]
giCbs TargetSrc
gSrc)
  -- Relational Checking: the following only runs when the list of relational specs is not empty
  (ψ, γ'') <- foldM (consAssmRel cfg info) ([], γ') (gsAsmRel sSpc ++ gsRelation sSpc)
  mapM_ (consRelTop cfg info γ'' ψ) (gsRelation sSpc)
  -- End: Relational Checking
  mapM_ (consClass γ) (gsMethods $ gsSig $ giSpec info)
  hcs <- gets hsCs
  hws <- gets hsWfs
  fcs <- concat <$> mapM (splitC (typeclass (getConfig info))) hcs
  fws <- concat <$> mapM splitW hws
  checkStratCtors γ sSpc
  when (warnOnTermHoles cfg) emitConsolidatedHoleWarnings
  modify $ \CGInfo
st -> CGInfo
st { fEnv     = fEnv    st `mappend` feEnv (fenv γ)
                     , cgLits   = litEnv   γ
                     , cgConsts = cgConsts st `mappend` constEnv γ
                     , fixCs    = fcs
                     , fixWfs   = fws }


---------------------------------
-- | Checking stratified ctors --
---------------------------------
type FExpr = F.ExprV F.Symbol
type Ctors = S.HashSet F.Symbol

checkStratCtors :: CGEnv -> GhcSpecSig -> CG ()
checkStratCtors :: CGEnv -> GhcSpecSig -> State CGInfo ()
checkStratCtors CGEnv
env GhcSpecSig
sSpc = do
  let ctors :: HashSet Symbol
ctors = [Symbol] -> HashSet Symbol
forall a. Hashable a => [a] -> HashSet a
S.fromList ([Symbol] -> HashSet Symbol) -> [Symbol] -> HashSet Symbol
forall a b. (a -> b) -> a -> b
$ HashMap Symbol Sort -> [Symbol]
forall k v. HashMap k v -> [k]
M.keys (HashMap Symbol Sort -> [Symbol])
-> HashMap Symbol Sort -> [Symbol]
forall a b. (a -> b) -> a -> b
$ SEnvB Symbol Sort -> HashMap Symbol Sort
forall b a. SEnvB b a -> HashMap b a
F.seBinds (SEnvB Symbol Sort -> HashMap Symbol Sort)
-> SEnvB Symbol Sort -> HashMap Symbol Sort
forall a b. (a -> b) -> a -> b
$ CGEnv -> SEnvB Symbol Sort
constEnv CGEnv
env
  let ctorRefinements :: [(Var, LocSpecType)]
ctorRefinements = ((Var, LocSpecType) -> Bool)
-> [(Var, LocSpecType)] -> [(Var, LocSpecType)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Var -> Bool
isStrat (Var -> Bool)
-> ((Var, LocSpecType) -> Var) -> (Var, LocSpecType) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Var, LocSpecType) -> Var
forall a b. (a, b) -> a
fst) ([(Var, LocSpecType)] -> [(Var, LocSpecType)])
-> [(Var, LocSpecType)] -> [(Var, LocSpecType)]
forall a b. (a -> b) -> a -> b
$ GhcSpecSig -> [(Var, LocSpecType)]
gsTySigs GhcSpecSig
sSpc
  [(Var, LocSpecType)]
-> ((Var, LocSpecType) -> State CGInfo ()) -> State CGInfo ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(Var, LocSpecType)]
ctorRefinements (((Var, LocSpecType) -> State CGInfo ()) -> State CGInfo ())
-> ((Var, LocSpecType) -> State CGInfo ()) -> State CGInfo ()
forall a b. (a -> b) -> a -> b
$ (Var -> LocSpecType -> State CGInfo ())
-> (Var, LocSpecType) -> State CGInfo ()
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((Var -> LocSpecType -> State CGInfo ())
 -> (Var, LocSpecType) -> State CGInfo ())
-> (Var -> LocSpecType -> State CGInfo ())
-> (Var, LocSpecType)
-> State CGInfo ()
forall a b. (a -> b) -> a -> b
$ HashSet Symbol -> Var -> LocSpecType -> State CGInfo ()
checkCtor HashSet Symbol
ctors
  where
    -- (Alecs): For some reason it can't see that they are the same
    -- GHC name, probably is due to some worker wrapper shenannigans
    hack :: Name -> [Char]
hack = OccName -> [Char]
occNameString (OccName -> [Char]) -> (Name -> OccName) -> Name -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> OccName
nameOccName
    isStrat :: Var -> Bool
isStrat Var
nm = Name -> [Char]
hack (Var -> Name
varName Var
nm) [Char] -> [[Char]] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` (Name -> [Char]) -> [Name] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map Name -> [Char]
hack (GhcSpecSig -> [Name]
gsStratCtos GhcSpecSig
sSpc)

uncurryPi :: SpecType -> ([SpecType], SpecType)
uncurryPi :: SpecType -> ([SpecType], SpecType)
uncurryPi (RFun Symbol
_ RFInfo
_ SpecType
dom SpecType
cod RReft
_) = ([SpecType] -> [SpecType])
-> ([SpecType], SpecType) -> ([SpecType], SpecType)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (SpecType
dom SpecType -> [SpecType] -> [SpecType]
forall a. a -> [a] -> [a]
:) (([SpecType], SpecType) -> ([SpecType], SpecType))
-> ([SpecType], SpecType) -> ([SpecType], SpecType)
forall a b. (a -> b) -> a -> b
$ SpecType -> ([SpecType], SpecType)
uncurryPi SpecType
cod
uncurryPi SpecType
rest                 = ([], SpecType
rest)

getTyConName :: SpecType -> Name
getTyConName :: SpecType -> Name
getTyConName SpecType
a = TyCon -> Name
Ghc.tyConName (TyCon -> Name) -> TyCon -> Name
forall a b. (a -> b) -> a -> b
$ RTyCon -> TyCon
rtc_tc (RTyCon -> TyCon) -> RTyCon -> TyCon
forall a b. (a -> b) -> a -> b
$ SpecType -> RTyCon
forall b v c tv r. RTypeBV b v c tv r -> c
rt_tycon SpecType
a

checkCtor :: Ctors -> Var -> LocSpecType -> CG ()
checkCtor :: HashSet Symbol -> Var -> LocSpecType -> State CGInfo ()
checkCtor HashSet Symbol
ctors Var
name LocSpecType
typ = do
  let loc :: SrcSpan
loc = SourcePos -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan (SourcePos -> SrcSpan) -> SourcePos -> SrcSpan
forall a b. (a -> b) -> a -> b
$ LocSpecType -> SourcePos
forall a. Located a -> SourcePos
F.loc LocSpecType
typ
  let ([SpecType]
args, SpecType
ret) = SpecType -> ([SpecType], SpecType)
uncurryPi (SpecType -> ([SpecType], SpecType))
-> SpecType -> ([SpecType], SpecType)
forall a b. (a -> b) -> a -> b
$ LocSpecType -> SpecType
forall a. Located a -> a
val LocSpecType
typ
  -- The constuctor that we want not to appear negatively
  let tyName :: Name
tyName = SpecType -> Name
getTyConName SpecType
ret
  -- Its index information
  retIdx <- case ReftBV Symbol Symbol -> Maybe (ExprBV Symbol Symbol)
getPropIndex (ReftBV Symbol Symbol -> Maybe (ExprBV Symbol Symbol))
-> ReftBV Symbol Symbol -> Maybe (ExprBV Symbol Symbol)
forall a b. (a -> b) -> a -> b
$ RReft -> ReftBV Symbol Symbol
forall b v r. UReftBV b v r -> r
ur_reft (RReft -> ReftBV Symbol Symbol) -> RReft -> ReftBV Symbol Symbol
forall a b. (a -> b) -> a -> b
$ SpecType -> RReft
forall b v c tv r. RTypeBV b v c tv r -> r
rt_reft SpecType
ret of
    Just ExprBV Symbol Symbol
idx -> ExprBV Symbol Symbol
-> StateT CGInfo Identity (ExprBV Symbol Symbol)
forall a. a -> StateT CGInfo Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ExprBV Symbol Symbol
idx
    Maybe (ExprBV Symbol Symbol)
Nothing  -> UserError -> StateT CGInfo Identity (ExprBV Symbol Symbol)
forall a. UserError -> a
uError (UserError -> StateT CGInfo Identity (ExprBV Symbol Symbol))
-> UserError -> StateT CGInfo Identity (ExprBV Symbol Symbol)
forall a b. (a -> b) -> a -> b
$ SrcSpan -> Doc -> Doc -> Doc -> UserError
forall t. SrcSpan -> Doc -> Doc -> Doc -> TError t
ErrStratNotPropRet SrcSpan
loc (Name -> Doc
forall a. PPrint a => a -> Doc
pprint Name
tyName) (Var -> Doc
forall a. PPrint a => a -> Doc
pprint Var
name) (SpecType -> Doc
forall a. PPrint a => a -> Doc
F.pprint SpecType
ret)
  -- For every argument of the constructor we check that all the
  -- self-refernce are refined by a "smaller" `prop` annotation
  forM_ args $ checkNg ctors loc name tyName retIdx

checkNg :: Ctors -> SrcSpan -> Var -> Name -> FExpr -> SpecType -> CG ()
checkNg :: HashSet Symbol
-> SrcSpan
-> Var
-> Name
-> ExprBV Symbol Symbol
-> SpecType
-> State CGInfo ()
checkNg HashSet Symbol
ctors SrcSpan
loc Var
ctorName Name
tyName ExprBV Symbol Symbol
retIdx = SpecType -> State CGInfo ()
go
  where
    go :: SpecType -> CG ()
    go :: SpecType -> State CGInfo ()
go RVar {} = () -> State CGInfo ()
forall a. a -> StateT CGInfo Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    go RAllT { SpecType
rt_ty :: SpecType
rt_ty :: forall b v c tv r. RTypeBV b v c tv r -> RTypeBV b v c tv r
rt_ty } = SpecType -> State CGInfo ()
go SpecType
rt_ty
    go RAllP { SpecType
rt_ty :: forall b v c tv r. RTypeBV b v c tv r -> RTypeBV b v c tv r
rt_ty :: SpecType
rt_ty } = SpecType -> State CGInfo ()
go SpecType
rt_ty
    go RFun { SpecType
rt_in :: SpecType
rt_in :: forall b v c tv r. RTypeBV b v c tv r -> RTypeBV b v c tv r
rt_in, SpecType
rt_out :: SpecType
rt_out :: forall b v c tv r. RTypeBV b v c tv r -> RTypeBV b v c tv r
rt_out } = do
      SpecType -> State CGInfo ()
go SpecType
rt_in
      SpecType -> State CGInfo ()
go SpecType
rt_out
    go r :: SpecType
r@RApp { rt_tycon :: forall b v c tv r. RTypeBV b v c tv r -> c
rt_tycon = RTyCon { TyCon
rtc_tc :: RTyCon -> TyCon
rtc_tc :: TyCon
rtc_tc }, [SpecType]
rt_args :: [SpecType]
rt_args :: forall b v c tv r. RTypeBV b v c tv r -> [RTypeBV b v c tv r]
rt_args, RReft
rt_reft :: forall b v c tv r. RTypeBV b v c tv r -> r
rt_reft :: RReft
rt_reft } = do
      if TyCon -> Name
Ghc.tyConName TyCon
rtc_tc Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
tyName then do
          case ReftBV Symbol Symbol -> Maybe (ExprBV Symbol Symbol)
getPropIndex (ReftBV Symbol Symbol -> Maybe (ExprBV Symbol Symbol))
-> ReftBV Symbol Symbol -> Maybe (ExprBV Symbol Symbol)
forall a b. (a -> b) -> a -> b
$ RReft -> ReftBV Symbol Symbol
forall b v r. UReftBV b v r -> r
ur_reft RReft
rt_reft of
            (Just ExprBV Symbol Symbol
arg) -> do
              -- We compare index information The occurrence is safe
              -- iff the index of the return type is strictly bigger
              -- than the one in negative position
              Bool -> State CGInfo () -> State CGInfo ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (HashSet Symbol
-> ExprBV Symbol Symbol -> ExprBV Symbol Symbol -> Bool
isStructurallySmaller HashSet Symbol
ctors ExprBV Symbol Symbol
arg ExprBV Symbol Symbol
retIdx) (State CGInfo () -> State CGInfo ())
-> State CGInfo () -> State CGInfo ()
forall a b. (a -> b) -> a -> b
$ do
                UserError -> State CGInfo ()
forall a. UserError -> a
uError (UserError -> State CGInfo ()) -> UserError -> State CGInfo ()
forall a b. (a -> b) -> a -> b
$ SrcSpan -> Doc -> Doc -> Doc -> Doc -> UserError
forall t. SrcSpan -> Doc -> Doc -> Doc -> Doc -> TError t
ErrStratIdxNotSmall SrcSpan
loc
                  (Name -> Doc
forall a. PPrint a => a -> Doc
pprint Name
tyName) (Var -> Doc
forall a. PPrint a => a -> Doc
pprint Var
ctorName) (ExprBV Symbol Symbol -> Doc
forall a. PPrint a => a -> Doc
F.pprint ExprBV Symbol Symbol
retIdx) (ExprBV Symbol Symbol -> Doc
forall a. PPrint a => a -> Doc
F.pprint ExprBV Symbol Symbol
arg)
            -- We don't have index information for both so we bail
            Maybe (ExprBV Symbol Symbol)
_ -> UserError -> State CGInfo ()
forall a. UserError -> a
uError (UserError -> State CGInfo ()) -> UserError -> State CGInfo ()
forall a b. (a -> b) -> a -> b
$ SrcSpan -> Doc -> Doc -> Doc -> UserError
forall t. SrcSpan -> Doc -> Doc -> Doc -> TError t
ErrStratOccProp SrcSpan
loc (Name -> Doc
forall a. PPrint a => a -> Doc
pprint Name
tyName) (Var -> Doc
forall a. PPrint a => a -> Doc
pprint Var
ctorName) (SpecType -> Doc
forall a. PPrint a => a -> Doc
F.pprint SpecType
r)
      else do
        [SpecType] -> (SpecType -> State CGInfo ()) -> State CGInfo ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [SpecType]
rt_args SpecType -> State CGInfo ()
go
    go SpecType
_ = Identity () -> State CGInfo ()
forall (m :: * -> *) a. Monad m => m a -> StateT CGInfo m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Identity () -> State CGInfo ()) -> Identity () -> State CGInfo ()
forall a b. (a -> b) -> a -> b
$ Maybe SrcSpan -> [Char] -> Identity ()
forall a. Maybe SrcSpan -> [Char] -> a
impossible (SrcSpan -> Maybe SrcSpan
forall a. a -> Maybe a
Just SrcSpan
loc) [Char]
"checkNg unexpected type"


isStructurallySmaller :: Ctors -> FExpr -> FExpr -> Bool
isStructurallySmaller :: HashSet Symbol
-> ExprBV Symbol Symbol -> ExprBV Symbol Symbol -> Bool
isStructurallySmaller HashSet Symbol
ctors ExprBV Symbol Symbol
l ExprBV Symbol Symbol
r
  -- Congruence rule
  | (F.EVar Symbol
nl, [ExprBV Symbol Symbol]
argsl) <- ExprBV Symbol Symbol
-> (ExprBV Symbol Symbol, [ExprBV Symbol Symbol])
F.splitEAppThroughECst ExprBV Symbol Symbol
l
  , (F.EVar Symbol
nr, [ExprBV Symbol Symbol]
argsr) <- ExprBV Symbol Symbol
-> (ExprBV Symbol Symbol, [ExprBV Symbol Symbol])
F.splitEAppThroughECst ExprBV Symbol Symbol
r
  , Symbol
nl Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
nr
  , [ExprBV Symbol Symbol] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [ExprBV Symbol Symbol]
argsl Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [ExprBV Symbol Symbol] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [ExprBV Symbol Symbol]
argsr
  , Symbol
nl Symbol -> HashSet Symbol -> Bool
forall a. Eq a => a -> HashSet a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` HashSet Symbol
ctors
  = HashSet Symbol
-> [ExprBV Symbol Symbol] -> [ExprBV Symbol Symbol] -> Bool
lexOrder HashSet Symbol
ctors [ExprBV Symbol Symbol]
argsl [ExprBV Symbol Symbol]
argsr
  | Bool
otherwise = HashSet Symbol
-> ExprBV Symbol Symbol -> ExprBV Symbol Symbol -> Bool
isSubterm HashSet Symbol
ctors ExprBV Symbol Symbol
l ExprBV Symbol Symbol
r Bool -> Bool -> Bool
&& ExprBV Symbol Symbol
l ExprBV Symbol Symbol -> ExprBV Symbol Symbol -> Bool
forall a. Eq a => a -> a -> Bool
/= ExprBV Symbol Symbol
r

lexOrder :: Ctors -> [F.ExprV F.Symbol] -> [F.ExprV F.Symbol] -> Bool
lexOrder :: HashSet Symbol
-> [ExprBV Symbol Symbol] -> [ExprBV Symbol Symbol] -> Bool
lexOrder HashSet Symbol
_     []     []            = Bool
False
lexOrder HashSet Symbol
ctors (ExprBV Symbol Symbol
l:[ExprBV Symbol Symbol]
ls) (ExprBV Symbol Symbol
r:[ExprBV Symbol Symbol]
rs)
  | HashSet Symbol
-> ExprBV Symbol Symbol -> ExprBV Symbol Symbol -> Bool
isStructurallySmaller HashSet Symbol
ctors ExprBV Symbol Symbol
l ExprBV Symbol Symbol
r = Bool
True
  | ExprBV Symbol Symbol
l ExprBV Symbol Symbol -> ExprBV Symbol Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== ExprBV Symbol Symbol
r                          = HashSet Symbol
-> [ExprBV Symbol Symbol] -> [ExprBV Symbol Symbol] -> Bool
lexOrder HashSet Symbol
ctors [ExprBV Symbol Symbol]
ls [ExprBV Symbol Symbol]
rs
  | Bool
otherwise                       = Bool
False
lexOrder HashSet Symbol
_ [ExprBV Symbol Symbol]
_ [ExprBV Symbol Symbol]
_ = [Char] -> [Char] -> Bool
forall a. [Char] -> [Char] -> a
errorP [Char]
"" [Char]
"lexOrder: different length lists"

isSubterm :: Ctors -> FExpr -> FExpr -> Bool
isSubterm :: HashSet Symbol
-> ExprBV Symbol Symbol -> ExprBV Symbol Symbol -> Bool
isSubterm HashSet Symbol
ctors ExprBV Symbol Symbol
l ExprBV Symbol Symbol
r | ExprBV Symbol Symbol
l ExprBV Symbol Symbol -> ExprBV Symbol Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== ExprBV Symbol Symbol
r
                   = Bool
True
                  -- Congruence rule
                  | (F.EVar Symbol
nm, [ExprBV Symbol Symbol]
args) <- ExprBV Symbol Symbol
-> (ExprBV Symbol Symbol, [ExprBV Symbol Symbol])
F.splitEAppThroughECst ExprBV Symbol Symbol
r
                  , Symbol
nm Symbol -> HashSet Symbol -> Bool
forall a. Eq a => a -> HashSet a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` HashSet Symbol
ctors
                  = (ExprBV Symbol Symbol -> Bool) -> [ExprBV Symbol Symbol] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (HashSet Symbol
-> ExprBV Symbol Symbol -> ExprBV Symbol Symbol -> Bool
isSubterm HashSet Symbol
ctors ExprBV Symbol Symbol
l) [ExprBV Symbol Symbol]
args
                  | Bool
otherwise
                  = Bool
False

-- | Emit one warning per recorded term hole after constraint generation has
--   collected both the hole metadata and any ANF expressions linked to it.
--
-- See Note [Term holes]
emitConsolidatedHoleWarnings :: CG ()
emitConsolidatedHoleWarnings :: State CGInfo ()
emitConsolidatedHoleWarnings = do
  holes     <- (CGInfo
 -> HashMap (Var, SrcSpan) (HoleInfo (CGInfo, CGEnv) SpecType))
-> StateT
     CGInfo
     Identity
     (HashMap (Var, SrcSpan) (HoleInfo (CGInfo, CGEnv) SpecType))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CGInfo
-> HashMap (Var, SrcSpan) (HoleInfo (CGInfo, CGEnv) SpecType)
hsHoles
  holeExprs <- gets hsHolesExprs

  let mergedHoles
                  = [(Var
h
                    , HoleInfo (CGInfo, CGEnv) SpecType
holeInfo
                    , [(Var, Expr Var, SpecType)]
-> (Var, SrcSpan)
-> HashMap (Var, SrcSpan) [(Var, Expr Var, SpecType)]
-> [(Var, Expr Var, SpecType)]
forall k v. Hashable k => v -> k -> HashMap k v -> v
M.findWithDefault [] (Var
h, SrcSpan
srcSpan) HashMap (Var, SrcSpan) [(Var, Expr Var, SpecType)]
holeExprs
                    )
                    | ((Var
h, SrcSpan
srcSpan), HoleInfo (CGInfo, CGEnv) SpecType
holeInfo) <- HashMap (Var, SrcSpan) (HoleInfo (CGInfo, CGEnv) SpecType)
-> [((Var, SrcSpan), HoleInfo (CGInfo, CGEnv) SpecType)]
forall k v. HashMap k v -> [(k, v)]
M.toList HashMap (Var, SrcSpan) (HoleInfo (CGInfo, CGEnv) SpecType)
holes
                    ]

  forM_ mergedHoles $ \(Var
h, HoleInfo (CGInfo, CGEnv) SpecType
holeInfo, [(Var, Expr Var, SpecType)]
anfs) -> do
    let γ :: CGEnv
γ        = (CGInfo, CGEnv) -> CGEnv
forall a b. (a, b) -> b
snd ((CGInfo, CGEnv) -> CGEnv)
-> (HoleInfo (CGInfo, CGEnv) SpecType -> (CGInfo, CGEnv))
-> HoleInfo (CGInfo, CGEnv) SpecType
-> CGEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HoleInfo (CGInfo, CGEnv) SpecType -> (CGInfo, CGEnv)
forall i t. HoleInfo i t -> i
info (HoleInfo (CGInfo, CGEnv) SpecType -> CGEnv)
-> HoleInfo (CGInfo, CGEnv) SpecType -> CGEnv
forall a b. (a -> b) -> a -> b
$ HoleInfo (CGInfo, CGEnv) SpecType
holeInfo
    let anfs' :: [(Symbol, Expr Var, SpecType)]
anfs'    = ((Var, Expr Var, SpecType) -> (Symbol, Expr Var, SpecType))
-> [(Var, Expr Var, SpecType)] -> [(Symbol, Expr Var, SpecType)]
forall a b. (a -> b) -> [a] -> [b]
map (\(Var
v, Expr Var
x, SpecType
t) -> (Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
v, Expr Var
x, SpecType
t)) [(Var, Expr Var, SpecType)]
anfs
    Error -> State CGInfo ()
addWarning (Error -> State CGInfo ()) -> Error -> State CGInfo ()
forall a b. (a -> b) -> a -> b
$ SrcSpan
-> Doc
-> HashMap Symbol SpecType
-> Symbol
-> SpecType
-> [(Symbol, Expr Var, SpecType)]
-> Error
forall t.
SrcSpan
-> Doc
-> HashMap Symbol t
-> Symbol
-> t
-> [(Symbol, Expr Var, t)]
-> TError t
ErrHole (HoleInfo (CGInfo, CGEnv) SpecType -> SrcSpan
forall i t. HoleInfo i t -> SrcSpan
hloc HoleInfo (CGInfo, CGEnv) SpecType
holeInfo) Doc
"hole found" (AREnv SpecType -> HashMap Symbol SpecType
forall t. AREnv t -> HashMap Symbol t
reLocal (AREnv SpecType -> HashMap Symbol SpecType)
-> AREnv SpecType -> HashMap Symbol SpecType
forall a b. (a -> b) -> a -> b
$ CGEnv -> AREnv SpecType
renv CGEnv
γ) (Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
h) (HoleInfo (CGInfo, CGEnv) SpecType -> SpecType
forall i t. HoleInfo i t -> t
htype HoleInfo (CGInfo, CGEnv) SpecType
holeInfo) [(Symbol, Expr Var, SpecType)]
anfs'


--------------------------------------------------------------------------------
-- | Ensure that the instance type is a subtype of the class type --------------
--------------------------------------------------------------------------------

consClass :: CGEnv -> (Var, MethodType LocSpecType) -> CG ()
consClass :: CGEnv -> (Var, MethodType LocSpecType) -> State CGInfo ()
consClass CGEnv
γ (Var
x,MethodType LocSpecType
mt)
  | Just LocSpecType
ti <- MethodType LocSpecType -> Maybe LocSpecType
forall t. MethodType t -> Maybe t
tyInstance MethodType LocSpecType
mt
  , Just LocSpecType
tc <- MethodType LocSpecType -> Maybe LocSpecType
forall t. MethodType t -> Maybe t
tyClass    MethodType LocSpecType
mt
  = SubC -> [Char] -> State CGInfo ()
addC (CGEnv -> SpecType -> SpecType -> SubC
SubC (CGEnv
γ CGEnv -> Span -> CGEnv
`setLocation` SrcSpan -> Span
Sp.Span (SourcePos -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan (LocSpecType -> SourcePos
forall a. Located a -> SourcePos
F.loc LocSpecType
ti))) (LocSpecType -> SpecType
forall a. Located a -> a
val LocSpecType
ti) (LocSpecType -> SpecType
forall a. Located a -> a
val LocSpecType
tc)) ([Char]
"cconsClass for " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Var -> [Char]
forall a. Outputable a => a -> [Char]
GM.showPpr Var
x)
consClass CGEnv
_ (Var, MethodType LocSpecType)
_
  = () -> State CGInfo ()
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

--------------------------------------------------------------------------------
consCBLet :: CGEnv -> CoreBind -> CG CGEnv
--------------------------------------------------------------------------------
consCBLet :: CGEnv -> Bind Var -> CG CGEnv
consCBLet CGEnv
γ Bind Var
cb = do
  oldtcheck <- (CGInfo -> Bool) -> StateT CGInfo Identity Bool
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CGInfo -> Bool
tcheck
  isStr     <- doTermCheck (getConfig γ) cb
  -- TODO: yuck.
  modify $ \CGInfo
s -> CGInfo
s { tcheck = oldtcheck && isStr }
  γ' <- consCB (mkTCheck oldtcheck isStr) γ cb
  modify $ \CGInfo
s -> CGInfo
s{tcheck = oldtcheck}
  return γ'

--------------------------------------------------------------------------------
-- | Constraint Generation: Corebind -------------------------------------------
--------------------------------------------------------------------------------
consCBTop :: Config -> TargetInfo -> CGEnv -> CoreBind -> CG CGEnv
--------------------------------------------------------------------------------
consCBTop :: Config -> TargetInfo -> CGEnv -> Bind Var -> CG CGEnv
consCBTop Config
cfg TargetInfo
info CGEnv
cgenv Bind Var
cb
  | (Var -> Bool) -> [Var] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Var -> Bool
trustVar [Var]
xs
  = (CGEnv -> Var -> CG CGEnv) -> CGEnv -> [Var] -> CG CGEnv
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM CGEnv -> Var -> CG CGEnv
addB CGEnv
cgenv [Var]
xs
    where
       xs :: [Var]
xs   = Bind Var -> [Var]
forall b. Bind b -> [b]
bindersOf Bind Var
cb
       tt :: Var -> StateT CGInfo Identity SpecType
tt   = Bool -> Type -> StateT CGInfo Identity SpecType
trueTy (Config -> Bool
typeclass Config
cfg) (Type -> StateT CGInfo Identity SpecType)
-> (Var -> Type) -> Var -> StateT CGInfo Identity SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> Type
varType
       addB :: CGEnv -> Var -> CG CGEnv
addB CGEnv
γ Var
x = Var -> StateT CGInfo Identity SpecType
tt Var
x StateT CGInfo Identity SpecType
-> (SpecType -> CG CGEnv) -> CG CGEnv
forall a b.
StateT CGInfo Identity a
-> (a -> StateT CGInfo Identity b) -> StateT CGInfo Identity b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (\SpecType
t -> CGEnv
γ CGEnv -> ([Char], Symbol, SpecType) -> CG CGEnv
+= ([Char]
"derived", Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
x, SpecType
t))
       trustVar :: Var -> Bool
trustVar Var
x = Bool -> Bool
not (Config -> Bool
checkDerived Config
cfg) Bool -> Bool -> Bool
&& TargetSrc -> Var -> Bool
derivedVar (TargetInfo -> TargetSrc
giSrc TargetInfo
info) Var
x

consCBTop Config
_ TargetInfo
_ CGEnv
γ Bind Var
cb
  = do oldtcheck <- (CGInfo -> Bool) -> StateT CGInfo Identity Bool
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CGInfo -> Bool
tcheck
       -- lazyVars  <- specLazy <$> get
       isStr     <- doTermCheck (getConfig γ) cb
       modify $ \CGInfo
s -> CGInfo
s { tcheck = oldtcheck && isStr}
       -- remove invariants that came from the cb definition
       let (γ', i) = removeInvariant γ cb                 --- DIFF
       γ'' <- consCB (mkTCheck oldtcheck isStr) (γ'{cgVar = topBind cb}) cb
       modify $ \CGInfo
s -> CGInfo
s { tcheck = oldtcheck}
       return $ restoreInvariant γ'' i                    --- DIFF
    where
      topBind :: Bind a -> Maybe a
topBind (NonRec a
v Expr a
_)  = a -> Maybe a
forall a. a -> Maybe a
Just a
v
      topBind (Rec [(a
v,Expr a
_)]) = a -> Maybe a
forall a. a -> Maybe a
Just a
v
      topBind Bind a
_             = Maybe a
forall a. Maybe a
Nothing

--------------------------------------------------------------------------------
consCB :: TCheck -> CGEnv -> CoreBind -> CG CGEnv
--------------------------------------------------------------------------------
-- do termination checking
consCB :: TCheck -> CGEnv -> Bind Var -> CG CGEnv
consCB TCheck
TerminationCheck CGEnv
γ (Rec [(Var, Expr Var)]
xes)
  = do texprs <- (CGInfo -> HashMap Var [Located (ExprBV Symbol Symbol)])
-> StateT
     CGInfo Identity (HashMap Var [Located (ExprBV Symbol Symbol)])
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CGInfo -> HashMap Var [Located (ExprBV Symbol Symbol)]
termExprs
       modify $ \CGInfo
i -> CGInfo
i { recCount = recCount i + length xes }
       let xxes = (Var -> Maybe (Var, [Located (ExprBV Symbol Symbol)]))
-> [Var] -> [(Var, [Located (ExprBV Symbol Symbol)])]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (Var
-> HashMap Var [Located (ExprBV Symbol Symbol)]
-> Maybe (Var, [Located (ExprBV Symbol Symbol)])
forall {k} {a}. Hashable k => k -> HashMap k a -> Maybe (k, a)
`lookup'` HashMap Var [Located (ExprBV Symbol Symbol)]
texprs) [Var]
xs
       if null xxes
         then consCBSizedTys consBind γ xes
         else check xxes <$> consCBWithExprs consBind γ xes
    where
      xs :: [Var]
xs = ((Var, Expr Var) -> Var) -> [(Var, Expr Var)] -> [Var]
forall a b. (a -> b) -> [a] -> [b]
map (Var, Expr Var) -> Var
forall a b. (a, b) -> a
fst [(Var, Expr Var)]
xes
      check :: t a -> p -> p
check t a
ys p
r | t a -> Int
forall a. t a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length t a
ys Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Var] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Var]
xs = p
r
                 | Bool
otherwise              = Maybe SrcSpan -> [Char] -> p
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic (SrcSpan -> Maybe SrcSpan
forall a. a -> Maybe a
Just SrcSpan
loc) [Char]
forall {a}. IsString a => a
msg
      msg :: a
msg        = a
"Termination expressions must be provided for all mutually recursive binders"
      loc :: SrcSpan
loc        = Var -> SrcSpan
forall a. NamedThing a => a -> SrcSpan
getSrcSpan ([Var] -> Var
forall a. HasCallStack => [a] -> a
head [Var]
xs)
      lookup' :: k -> HashMap k a -> Maybe (k, a)
lookup' k
k HashMap k a
m = (k
k,) (a -> (k, a)) -> Maybe a -> Maybe (k, a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> k -> HashMap k a -> Maybe a
forall k v. Hashable k => k -> HashMap k v -> Maybe v
M.lookup k
k HashMap k a
m

-- don't do termination checking, but some strata checks?
consCB TCheck
StrataCheck CGEnv
γ (Rec [(Var, Expr Var)]
xes)
  = do xets     <- [(Var, Expr Var)]
-> ((Var, Expr Var)
    -> StateT CGInfo Identity (Var, Expr Var, Template SpecType))
-> StateT CGInfo Identity [(Var, Expr Var, Template SpecType)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Var, Expr Var)]
xes (((Var, Expr Var)
  -> StateT CGInfo Identity (Var, Expr Var, Template SpecType))
 -> StateT CGInfo Identity [(Var, Expr Var, Template SpecType)])
-> ((Var, Expr Var)
    -> StateT CGInfo Identity (Var, Expr Var, Template SpecType))
-> StateT CGInfo Identity [(Var, Expr Var, Template SpecType)]
forall a b. (a -> b) -> a -> b
$ \(Var
x, Expr Var
e) -> (Var
x, Expr Var
e,) (Template SpecType -> (Var, Expr Var, Template SpecType))
-> CG (Template SpecType)
-> StateT CGInfo Identity (Var, Expr Var, Template SpecType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CGEnv -> (Var, Maybe (Expr Var)) -> CG (Template SpecType)
varTemplate CGEnv
γ (Var
x, Expr Var -> Maybe (Expr Var)
forall a. a -> Maybe a
Just Expr Var
e)
       modify     $ \CGInfo
i -> CGInfo
i { recCount = recCount i + length xes }
       let xts    = [(Var
x, Template SpecType
to) | (Var
x, Expr Var
_, Template SpecType
to) <- [(Var, Expr Var, Template SpecType)]
xets]
       γ'        <- foldM extender (γ `setRecs` (fst <$> xts)) xts
       mapM_ (consBind True γ') xets
       return γ'

-- don't do termination checking, and don't do any strata checks either?
consCB TCheck
NoCheck CGEnv
γ (Rec [(Var, Expr Var)]
xes)
  = do xets   <- [(Var, Expr Var)]
-> ((Var, Expr Var)
    -> StateT CGInfo Identity (Var, Expr Var, Template SpecType))
-> StateT CGInfo Identity [(Var, Expr Var, Template SpecType)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Var, Expr Var)]
xes (((Var, Expr Var)
  -> StateT CGInfo Identity (Var, Expr Var, Template SpecType))
 -> StateT CGInfo Identity [(Var, Expr Var, Template SpecType)])
-> ((Var, Expr Var)
    -> StateT CGInfo Identity (Var, Expr Var, Template SpecType))
-> StateT CGInfo Identity [(Var, Expr Var, Template SpecType)]
forall a b. (a -> b) -> a -> b
$ \(Var
x, Expr Var
e) -> (Template SpecType -> (Var, Expr Var, Template SpecType))
-> CG (Template SpecType)
-> StateT CGInfo Identity (Var, Expr Var, Template SpecType)
forall a b.
(a -> b) -> StateT CGInfo Identity a -> StateT CGInfo Identity b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Var
x, Expr Var
e,) (CGEnv -> (Var, Maybe (Expr Var)) -> CG (Template SpecType)
varTemplate CGEnv
γ (Var
x, Expr Var -> Maybe (Expr Var)
forall a. a -> Maybe a
Just Expr Var
e))
       modify $ \CGInfo
i -> CGInfo
i { recCount = recCount i + length xes }
       let xts = [(Var
x, Template SpecType
to) | (Var
x, Expr Var
_, Template SpecType
to) <- [(Var, Expr Var, Template SpecType)]
xets]
       γ'     <- foldM extender (γ `setRecs` (fst <$> xts)) xts
       mapM_ (consBind True γ') xets
       return γ'

-- | NV: Dictionaries are not checked, because
-- | class methods' preconditions are not satisfied
consCB TCheck
_ CGEnv
γ (NonRec Var
x Expr Var
_) | Var -> Bool
isDictionary Var
x
  = do t  <- Bool -> Type -> StateT CGInfo Identity SpecType
trueTy (Config -> Bool
typeclass (CGEnv -> Config
forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)) (Var -> Type
varType Var
x)
       extender γ (x, Assumed t)
    where
       isDictionary :: Var -> Bool
isDictionary = Maybe (HashMap Symbol (RISig SpecType)) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (HashMap Symbol (RISig SpecType)) -> Bool)
-> (Var -> Maybe (HashMap Symbol (RISig SpecType))) -> Var -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DEnv Var SpecType -> Var -> Maybe (HashMap Symbol (RISig SpecType))
forall k t.
(Eq k, Hashable k) =>
DEnv k t -> k -> Maybe (HashMap Symbol (RISig t))
dlookup (CGEnv -> DEnv Var SpecType
denv CGEnv
γ)

consCB TCheck
_ CGEnv
γ (NonRec Var
x Expr Var
def)
  | Just (Var
w, [Type]
τ) <- Expr Var -> Maybe (Var, [Type])
grepDictionary Expr Var
def
  , Just HashMap Symbol (RISig SpecType)
d      <- DEnv Var SpecType -> Var -> Maybe (HashMap Symbol (RISig SpecType))
forall k t.
(Eq k, Hashable k) =>
DEnv k t -> k -> Maybe (HashMap Symbol (RISig t))
dlookup (CGEnv -> DEnv Var SpecType
denv CGEnv
γ) Var
w
  = do st       <- (Type -> StateT CGInfo Identity SpecType)
-> [Type] -> StateT CGInfo Identity [SpecType]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Bool -> Type -> StateT CGInfo Identity SpecType
trueTy (Config -> Bool
typeclass (CGEnv -> Config
forall t. HasConfig t => t -> Config
getConfig CGEnv
γ))) [Type]
τ
       mapM_ addW (WfC γ <$> st)
       let xts   = (RISig SpecType -> RISig SpecType)
-> HashMap Symbol (RISig SpecType)
-> HashMap Symbol (RISig SpecType)
forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
dmap ((SpecType -> SpecType) -> RISig SpecType -> RISig SpecType
forall a b. (a -> b) -> RISig a -> RISig b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([SpecType] -> SpecType -> SpecType
forall {r} {c} {tv} {b} {v}.
(IsReft r, TyConable c, FreeVar c tv,
 SubsTy tv (RTypeBV b v c tv (NoReftB b)) c,
 SubsTy tv (RTypeBV b v c tv (NoReftB b)) r,
 SubsTy tv (RTypeBV b v c tv (NoReftB b)) tv,
 SubsTy
   tv (RTypeBV b v c tv (NoReftB b)) (RTypeBV b v c tv (NoReftB b)),
 SubsTy
   tv
   (RTypeBV b v c tv (NoReftB b))
   (RTVar tv (RTypeBV b v c tv (NoReftB b))),
 Binder b, Hashable tv) =>
[RTypeBV b v c tv r] -> RTypeBV b v c tv r -> RTypeBV b v c tv r
f [SpecType]
st)) HashMap Symbol (RISig SpecType)
d
       let  γ'   = CGEnv
γ { denv = dinsert (denv γ) x xts }
       t        <- trueTy (typeclass (getConfig γ)) (varType x)
       extender γ' (x, Assumed t)
   where
    f :: [RTypeBV b v c tv r] -> RTypeBV b v c tv r -> RTypeBV b v c tv r
f [RTypeBV b v c tv r
t']    (RAllT RTVar tv (RTypeBV b v c tv (NoReftB b))
α RTypeBV b v c tv r
te r
_) = (tv, RTypeBV b v c tv r)
-> RTypeBV b v c tv r -> RTypeBV b v c tv r
forall tv r c b v.
(Eq tv, Hashable tv, IsReft r, TyConable c, Binder b,
 SubsTy tv (RTypeBV b v c tv (NoReftB b)) c,
 SubsTy tv (RTypeBV b v c tv (NoReftB b)) r,
 SubsTy
   tv (RTypeBV b v c tv (NoReftB b)) (RTypeBV b v c tv (NoReftB b)),
 FreeVar c tv, SubsTy tv (RTypeBV b v c tv (NoReftB b)) tv,
 SubsTy
   tv
   (RTypeBV b v c tv (NoReftB b))
   (RTVar tv (RTypeBV b v c tv (NoReftB b)))) =>
(tv, RTypeBV b v c tv r)
-> RTypeBV b v c tv r -> RTypeBV b v c tv r
subsTyVarMeet' (RTVar tv (RTypeBV b v c tv (NoReftB b)) -> tv
forall tv s. RTVar tv s -> tv
ty_var_value RTVar tv (RTypeBV b v c tv (NoReftB b))
α, RTypeBV b v c tv r
t') RTypeBV b v c tv r
te
    f (RTypeBV b v c tv r
t':[RTypeBV b v c tv r]
ts) (RAllT RTVar tv (RTypeBV b v c tv (NoReftB b))
α RTypeBV b v c tv r
te r
_) = [RTypeBV b v c tv r] -> RTypeBV b v c tv r -> RTypeBV b v c tv r
f [RTypeBV b v c tv r]
ts (RTypeBV b v c tv r -> RTypeBV b v c tv r)
-> RTypeBV b v c tv r -> RTypeBV b v c tv r
forall a b. (a -> b) -> a -> b
$ (tv, RTypeBV b v c tv r)
-> RTypeBV b v c tv r -> RTypeBV b v c tv r
forall tv r c b v.
(Eq tv, Hashable tv, IsReft r, TyConable c, Binder b,
 SubsTy tv (RTypeBV b v c tv (NoReftB b)) c,
 SubsTy tv (RTypeBV b v c tv (NoReftB b)) r,
 SubsTy
   tv (RTypeBV b v c tv (NoReftB b)) (RTypeBV b v c tv (NoReftB b)),
 FreeVar c tv, SubsTy tv (RTypeBV b v c tv (NoReftB b)) tv,
 SubsTy
   tv
   (RTypeBV b v c tv (NoReftB b))
   (RTVar tv (RTypeBV b v c tv (NoReftB b)))) =>
(tv, RTypeBV b v c tv r)
-> RTypeBV b v c tv r -> RTypeBV b v c tv r
subsTyVarMeet' (RTVar tv (RTypeBV b v c tv (NoReftB b)) -> tv
forall tv s. RTVar tv s -> tv
ty_var_value RTVar tv (RTypeBV b v c tv (NoReftB b))
α, RTypeBV b v c tv r
t') RTypeBV b v c tv r
te
    f [RTypeBV b v c tv r]
_ RTypeBV b v c tv r
_ = Maybe SrcSpan -> [Char] -> RTypeBV b v c tv r
forall a. Maybe SrcSpan -> [Char] -> a
impossible Maybe SrcSpan
forall a. Maybe a
Nothing [Char]
"consCB on Dictionary: this should not happen"

consCB TCheck
_ CGEnv
γ (NonRec Var
x Expr Var
e)
  = do to  <- CGEnv -> (Var, Maybe (Expr Var)) -> CG (Template SpecType)
varTemplate CGEnv
γ (Var
x, Maybe (Expr Var)
forall a. Maybe a
Nothing)
       when (warnOnTermHoles (getConfig γ)) checkLetHole
       to' <- consBind False γ (x, e, to) >>= addPostTemplate γ
       extender γ (x, makeSingleton γ (simplify e) <$> to')
  where
    -- See Note [Term holes]
    checkLetHole :: State CGInfo ()
checkLetHole =
      do
        let isItHole :: Maybe (RealSrcSpan, Var)
isItHole = Expr Var -> Maybe (RealSrcSpan, Var)
detectTypedHole Expr Var
e
        case Maybe (RealSrcSpan, Var)
isItHole of
          Just (RealSrcSpan
srcSpan, Var
var) -> do
            Var -> (Var, SrcSpan) -> State CGInfo ()
linkANFToHole Var
x (Var
var, RealSrcSpan -> Maybe BufSpan -> SrcSpan
RealSrcSpan RealSrcSpan
srcSpan Maybe BufSpan
forall a. Maybe a
Strict.Nothing)
          Maybe (RealSrcSpan, Var)
_ -> () -> State CGInfo ()
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
grepDictionary :: CoreExpr -> Maybe (Var, [Type])
grepDictionary :: Expr Var -> Maybe (Var, [Type])
grepDictionary = [Type] -> Expr Var -> Maybe (Var, [Type])
forall {b}. [Type] -> Expr b -> Maybe (Var, [Type])
go []
  where
    go :: [Type] -> Expr b -> Maybe (Var, [Type])
go [Type]
ts (App (Var Var
w) (Type Type
t)) = (Var, [Type]) -> Maybe (Var, [Type])
forall a. a -> Maybe a
Just (Var
w, [Type] -> [Type]
forall a. [a] -> [a]
reverse (Type
tType -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:[Type]
ts))
    go [Type]
ts (App Expr b
e (Type Type
t))       = [Type] -> Expr b -> Maybe (Var, [Type])
go (Type
tType -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:[Type]
ts) Expr b
e
    go [Type]
ts (App Expr b
e (Var Var
_))        = [Type] -> Expr b -> Maybe (Var, [Type])
go [Type]
ts Expr b
e
    go [Type]
ts (Let Bind b
_ Expr b
e)              = [Type] -> Expr b -> Maybe (Var, [Type])
go [Type]
ts Expr b
e
    go [Type]
_ Expr b
_                       = Maybe (Var, [Type])
forall a. Maybe a
Nothing

--------------------------------------------------------------------------------
consBind :: Bool -> CGEnv -> (Var, CoreExpr, Template SpecType) -> CG (Template SpecType)
--------------------------------------------------------------------------------
consBind :: Bool
-> CGEnv
-> (Var, Expr Var, Template SpecType)
-> CG (Template SpecType)
consBind Bool
_ CGEnv
_ (Var
x, Expr Var
_, Assumed SpecType
t)
  | RecSelId {} <- HasCallStack => Var -> IdDetails
Var -> IdDetails
idDetails Var
x -- don't check record selectors with assumed specs
  = Template SpecType -> CG (Template SpecType)
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Template SpecType -> CG (Template SpecType))
-> Template SpecType -> CG (Template SpecType)
forall a b. (a -> b) -> a -> b
$ [Char] -> Template SpecType -> Template SpecType
forall a. PPrint a => [Char] -> a -> a
F.notracepp ([Char]
"TYPE FOR SELECTOR " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Var -> [Char]
forall a. Show a => a -> [Char]
show Var
x) (Template SpecType -> Template SpecType)
-> Template SpecType -> Template SpecType
forall a b. (a -> b) -> a -> b
$ SpecType -> Template SpecType
forall a. a -> Template a
Assumed SpecType
t

consBind Bool
isRec' CGEnv
γ (Var
x, Expr Var
e, Asserted SpecType
spect)
  = do let γ' :: CGEnv
γ'       = CGEnv
γ CGEnv -> Var -> CGEnv
`setBind` Var
x
           ([(RTVar RTyVar (RTypeBV Symbol Symbol RTyCon RTyVar NoReft),
  RReft)]
_,[PVarBV Symbol Symbol (RTypeBV Symbol Symbol RTyCon RTyVar NoReft)]
πs,SpecType
_) = SpecType
-> ([(RTVar RTyVar (RTypeBV Symbol Symbol RTyCon RTyVar NoReft),
      RReft)],
    [PVarBV
       Symbol Symbol (RTypeBV Symbol Symbol RTyCon RTyVar NoReft)],
    SpecType)
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 SpecType
spect
       cgenv    <- (CGEnv
 -> PVarBV
      Symbol Symbol (RTypeBV Symbol Symbol RTyCon RTyVar NoReft)
 -> CG CGEnv)
-> CGEnv
-> [PVarBV
      Symbol Symbol (RTypeBV Symbol Symbol RTyCon RTyVar NoReft)]
-> CG CGEnv
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM CGEnv
-> PVarBV
     Symbol Symbol (RTypeBV Symbol Symbol RTyCon RTyVar NoReft)
-> CG CGEnv
addPToEnv CGEnv
γ' [PVarBV Symbol Symbol (RTypeBV Symbol Symbol RTyCon RTyVar NoReft)]
πs
       cconsE cgenv e (weakenResult (typeclass (getConfig γ)) x spect)
       when (F.symbol x `elemHEnv` holes γ) $
         -- have to add the wf constraint here for HOLEs so we have the proper env
         addW $ WfC cgenv $ fmap killSubst spect
       addIdA x (defAnn isRec' spect)
       return $ Asserted spect

consBind Bool
isRec' CGEnv
γ (Var
x, Expr Var
e, Internal SpecType
spect)
  = do let γ' :: CGEnv
γ'       = CGEnv
γ CGEnv -> Var -> CGEnv
`setBind` Var
x
           ([(RTVar RTyVar (RTypeBV Symbol Symbol RTyCon RTyVar NoReft),
  RReft)]
_,[PVarBV Symbol Symbol (RTypeBV Symbol Symbol RTyCon RTyVar NoReft)]
πs,SpecType
_) = SpecType
-> ([(RTVar RTyVar (RTypeBV Symbol Symbol RTyCon RTyVar NoReft),
      RReft)],
    [PVarBV
       Symbol Symbol (RTypeBV Symbol Symbol RTyCon RTyVar NoReft)],
    SpecType)
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 SpecType
spect
       γπ    <- (CGEnv
 -> PVarBV
      Symbol Symbol (RTypeBV Symbol Symbol RTyCon RTyVar NoReft)
 -> CG CGEnv)
-> CGEnv
-> [PVarBV
      Symbol Symbol (RTypeBV Symbol Symbol RTyCon RTyVar NoReft)]
-> CG CGEnv
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM CGEnv
-> PVarBV
     Symbol Symbol (RTypeBV Symbol Symbol RTyCon RTyVar NoReft)
-> CG CGEnv
addPToEnv CGEnv
γ' [PVarBV Symbol Symbol (RTypeBV Symbol Symbol RTyCon RTyVar NoReft)]
πs
       let γπ' = CGEnv
γπ {cerr = Just $ ErrHMeas (getLocation γπ) (pprint x) (text explanation)}
       cconsE γπ' e spect
       when (F.symbol x `elemHEnv` holes γ) $
         -- have to add the wf constraint here for HOLEs so we have the proper env
         addW $ WfC γπ $ fmap killSubst spect
       addIdA x (defAnn isRec' spect)
       return $ Internal spect
  where
    explanation :: a
explanation = a
"Cannot give singleton type to the function definition."

consBind Bool
isRec' CGEnv
γ (Var
x, Expr Var
e, Assumed SpecType
spect)
  = do let γ' :: CGEnv
γ' = CGEnv
γ CGEnv -> Var -> CGEnv
`setBind` Var
x
       γπ    <- (CGEnv
 -> PVarBV
      Symbol Symbol (RTypeBV Symbol Symbol RTyCon RTyVar NoReft)
 -> CG CGEnv)
-> CGEnv
-> [PVarBV
      Symbol Symbol (RTypeBV Symbol Symbol RTyCon RTyVar NoReft)]
-> CG CGEnv
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM CGEnv
-> PVarBV
     Symbol Symbol (RTypeBV Symbol Symbol RTyCon RTyVar NoReft)
-> CG CGEnv
addPToEnv CGEnv
γ' [PVarBV Symbol Symbol (RTypeBV Symbol Symbol RTyCon RTyVar NoReft)]
πs
       cconsE γπ e =<< true (typeclass (getConfig γ)) spect
       addIdA x (defAnn isRec' spect)
       return $ Asserted spect
    where πs :: [PVarBV Symbol Symbol (RTypeBV Symbol Symbol RTyCon RTyVar NoReft)]
πs   = RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
-> [PVarBV
      Symbol Symbol (RTypeBV Symbol Symbol RTyCon RTyVar NoReft)]
forall b v c tv r.
RTypeRepBV b v c tv r
-> [PVarBV b v (RTypeBV b v c tv (NoReftB b))]
ty_preds (RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
 -> [PVarBV
       Symbol Symbol (RTypeBV Symbol Symbol RTyCon RTyVar NoReft)])
-> RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
-> [PVarBV
      Symbol Symbol (RTypeBV Symbol Symbol RTyCon RTyVar NoReft)]
forall a b. (a -> b) -> a -> b
$ SpecType -> RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
forall b v c tv r. RTypeBV b v c tv r -> RTypeRepBV b v c tv r
toRTypeRep SpecType
spect

consBind Bool
isRec' CGEnv
γ (Var
x, Expr Var
e, Template SpecType
Unknown)
  = do t'    <- CGEnv -> Expr Var -> StateT CGInfo Identity SpecType
consE (CGEnv
γ CGEnv -> Var -> CGEnv
`setBind` Var
x) Expr Var
e
       t     <- topSpecType x t'
       addIdA x (defAnn isRec' t)
       when (GM.isExternalId x) (addKuts x t)
       return $ Asserted t

killSubst :: RReft -> RReft
killSubst :: RReft -> RReft
killSubst = (ReftBV Symbol Symbol -> ReftBV Symbol Symbol) -> RReft -> RReft
forall a b.
(a -> b) -> UReftBV Symbol Symbol a -> UReftBV Symbol Symbol b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ReftBV Symbol Symbol -> ReftBV Symbol Symbol
killSubstReft

killSubstReft :: F.Reft -> F.Reft
killSubstReft :: ReftBV Symbol Symbol -> ReftBV Symbol Symbol
killSubstReft = (ExprBV Symbol Symbol -> ExprBV Symbol Symbol)
-> ReftBV Symbol Symbol -> ReftBV Symbol Symbol
forall t.
Visitable t =>
(ExprBV Symbol Symbol -> ExprBV Symbol Symbol) -> t -> t
trans ExprBV Symbol Symbol -> ExprBV Symbol Symbol
forall {b} {v}. Monoid (KVarSubst b v) => ExprBV b v -> ExprBV b v
ks
  where
    ks :: ExprBV b v -> ExprBV b v
ks (F.PKVar KVar
k HashMap Symbol Sort
_ KVarSubst b v
_) = KVar -> HashMap Symbol Sort -> KVarSubst b v -> ExprBV b v
forall b v.
KVar -> HashMap Symbol Sort -> KVarSubst b v -> ExprBV b v
F.PKVar KVar
k HashMap Symbol Sort
forall a. Monoid a => a
mempty KVarSubst b v
forall a. Monoid a => a
mempty
    ks ExprBV b v
p                = ExprBV b v
p

-- | Add a type variable → sort mapping to every PKVar in a SpecType.
-- Used during type application to record how type variables are instantiated,
-- so the solver can apply the correct sort substitution to qualifier solutions.
addTyVarSubToKVars :: F.Symbol -> F.Sort -> SpecType -> SpecType
addTyVarSubToKVars :: Symbol -> Sort -> SpecType -> SpecType
addTyVarSubToKVars Symbol
sym Sort
sort = (RReft -> RReft) -> SpecType -> SpecType
forall a b.
(a -> b)
-> RTypeBV Symbol Symbol RTyCon RTyVar a
-> RTypeBV Symbol Symbol RTyCon RTyVar b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((ReftBV Symbol Symbol -> ReftBV Symbol Symbol) -> RReft -> RReft
forall a b.
(a -> b) -> UReftBV Symbol Symbol a -> UReftBV Symbol Symbol b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((ExprBV Symbol Symbol -> ExprBV Symbol Symbol)
-> ReftBV Symbol Symbol -> ReftBV Symbol Symbol
forall t.
Visitable t =>
(ExprBV Symbol Symbol -> ExprBV Symbol Symbol) -> t -> t
trans ExprBV Symbol Symbol -> ExprBV Symbol Symbol
forall {b} {v}. ExprBV b v -> ExprBV b v
addSub))
  where
    addSub :: ExprBV b v -> ExprBV b v
addSub (F.PKVar KVar
k HashMap Symbol Sort
tsu KVarSubst b v
su) =
      let tsu' :: HashMap Symbol Sort
tsu' = (Sort -> Sort) -> HashMap Symbol Sort -> HashMap Symbol Sort
forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
M.map (Symbol -> Sort -> Sort -> Sort
F.applyCoercion Symbol
sym Sort
sort) HashMap Symbol Sort
tsu
       in KVar -> HashMap Symbol Sort -> KVarSubst b v -> ExprBV b v
forall b v.
KVar -> HashMap Symbol Sort -> KVarSubst b v -> ExprBV b v
F.PKVar KVar
k (Symbol -> Sort -> HashMap Symbol Sort -> HashMap Symbol Sort
forall k v. Hashable k => k -> v -> HashMap k v -> HashMap k v
M.insert Symbol
sym Sort
sort HashMap Symbol Sort
tsu') KVarSubst b v
su
    addSub ExprBV b v
e                  = ExprBV b v
e

defAnn :: Bool -> t -> Annot t
defAnn :: forall t. Bool -> t -> Annot t
defAnn Bool
True  = t -> Annot t
forall t. t -> Annot t
AnnRDf
defAnn Bool
False = t -> Annot t
forall t. t -> Annot t
AnnDef

addPToEnv :: CGEnv
          -> PVar RSort -> CG CGEnv
addPToEnv :: CGEnv
-> PVarBV
     Symbol Symbol (RTypeBV Symbol Symbol RTyCon RTyVar NoReft)
-> CG CGEnv
addPToEnv CGEnv
γ PVarBV Symbol Symbol (RTypeBV Symbol Symbol RTyCon RTyVar NoReft)
π
  = do γπ <- CGEnv
γ CGEnv -> ([Char], Symbol, SpecType) -> CG CGEnv
+= ([Char]
"addSpec1", PVarBV Symbol Symbol (RTypeBV Symbol Symbol RTyCon RTyVar NoReft)
-> Symbol
forall b v t. PVarBV b v t -> b
pname PVarBV Symbol Symbol (RTypeBV Symbol Symbol RTyCon RTyVar NoReft)
π, PVarBV Symbol Symbol (RTypeBV Symbol Symbol RTyCon RTyVar NoReft)
-> SpecType
forall r.
(PPrint r, IsReft r) =>
PVarBV Symbol Symbol (RTypeBV Symbol Symbol RTyCon RTyVar NoReft)
-> RRType r
pvarRType PVarBV Symbol Symbol (RTypeBV Symbol Symbol RTyCon RTyVar NoReft)
π)
       foldM (+=) γπ [("addSpec2", x, ofRSort t) | (t, x, _) <- pargs π]

-- | Detect a direct typed-hole occurrence in Core and recover the source span
--   that GHC attached to it, if present. The helper deliberately matches the
--   stable @.hole@ naming convention after stripping wrappers introduced by
--   desugaring and normalization.
--
-- See Note [Term holes]
detectTypedHole :: CoreExpr -> Maybe (RealSrcSpan, Var)
detectTypedHole :: Expr Var -> Maybe (RealSrcSpan, Var)
detectTypedHole Expr Var
e =
  case Expr Var -> Expr Var
stripTicks Expr Var
e of
    Var Var
x | Var -> Bool
isVarHole Var
x ->
      case Expr Var -> Maybe CoreTickish
forall b. Expr b -> Maybe CoreTickish
lastTick Expr Var
e of
        Just (SourceNote RealSrcSpan
src LexicalFastString
_) -> (RealSrcSpan, Var) -> Maybe (RealSrcSpan, Var)
forall a. a -> Maybe a
Just (RealSrcSpan
src, Var
x)
        Maybe CoreTickish
_                       -> Maybe (RealSrcSpan, Var)
forall a. Maybe a
Nothing
    Expr Var
_ -> Maybe (RealSrcSpan, Var)
forall a. Maybe a
Nothing

-- | Remove the outer application and tick wrappers that GHC places around a
--   hole so 'detectTypedHole' can inspect the underlying binder.
stripTicks :: CoreExpr -> CoreExpr
stripTicks :: Expr Var -> Expr Var
stripTicks (App (Tick CoreTickish
_ Expr Var
e) Expr Var
_) = Expr Var -> Expr Var
stripTicks Expr Var
e
stripTicks (Tick CoreTickish
_ Expr Var
e)         = Expr Var -> Expr Var
stripTicks Expr Var
e
stripTicks Expr Var
e          = Expr Var
e

-- | Traverse an expression and keep the innermost tick, which is the source
--   note used to report the hole location.
lastTick :: Expr b -> Maybe CoreTickish
lastTick :: forall b. Expr b -> Maybe CoreTickish
lastTick (Tick CoreTickish
t Expr b
e) =
  case Expr b -> Maybe CoreTickish
forall b. Expr b -> Maybe CoreTickish
lastTick Expr b
e of
    Just CoreTickish
t' -> CoreTickish -> Maybe CoreTickish
forall a. a -> Maybe a
Just CoreTickish
t'
    Maybe CoreTickish
Nothing -> CoreTickish -> Maybe CoreTickish
forall a. a -> Maybe a
Just CoreTickish
t
lastTick (App Expr b
e Expr b
a) =
  case Expr b -> Maybe CoreTickish
forall b. Expr b -> Maybe CoreTickish
lastTick Expr b
a of
    Just CoreTickish
ta -> CoreTickish -> Maybe CoreTickish
forall a. a -> Maybe a
Just CoreTickish
ta
    Maybe CoreTickish
Nothing -> Expr b -> Maybe CoreTickish
forall b. Expr b -> Maybe CoreTickish
lastTick Expr b
e
lastTick Expr b
_ = Maybe CoreTickish
forall a. Maybe a
Nothing

-- | Check whether a Core binder name follows GHC's @.hole@ naming scheme for
--   typed holes.
isVarHole :: Var -> Bool
isVarHole :: Var -> Bool
isVarHole Var
x = [Char] -> Bool
isHoleStr (Symbol -> [Char]
F.symbolString (Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
x))
  where
    isHoleStr :: [Char] -> Bool
isHoleStr [Char]
s =
      case (Char -> Bool) -> [Char] -> ([Char], [Char])
forall a. (a -> Bool) -> [a] -> ([a], [a])
break (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'.') [Char]
s of
        ([Char]
_, Char
'.':[Char]
rest) -> [Char]
rest [Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
== [Char]
"hole"
        ([Char], [Char])
_             -> Bool
False

--------------------------------------------------------------------------------
-- | Bidirectional Constraint Generation: CHECKING -----------------------------
--------------------------------------------------------------------------------
cconsE :: CGEnv -> CoreExpr -> SpecType -> CG ()
--------------------------------------------------------------------------------
cconsE :: CGEnv -> Expr Var -> SpecType -> State CGInfo ()
cconsE CGEnv
g Expr Var
e SpecType
t = do
  Expr Var -> SpecType -> State CGInfo ()
checkANFHoleInExpr Expr Var
e SpecType
t
  CGEnv -> Expr Var -> SpecType -> State CGInfo ()
cconsE' CGEnv
g Expr Var
e SpecType
t

--------------------------------------------------------------------------------
cconsE' :: CGEnv -> CoreExpr -> SpecType -> CG ()
--------------------------------------------------------------------------------
cconsE' :: CGEnv -> Expr Var -> SpecType -> State CGInfo ()
cconsE' CGEnv
γ Expr Var
e SpecType
t
  | Just (Rs.PatSelfBind Var
_x Expr Var
e') <- Expr Var -> Maybe Pattern
Rs.lift Expr Var
e
  = CGEnv -> Expr Var -> SpecType -> State CGInfo ()
cconsE' CGEnv
γ Expr Var
e' SpecType
t

  | Just (Rs.PatSelfRecBind Var
x Expr Var
e') <- Expr Var -> Maybe Pattern
Rs.lift Expr Var
e
  = let γ' :: CGEnv
γ' = CGEnv
γ { grtys = insertREnv (F.symbol x) t (grtys γ)}
    in CG CGEnv -> State CGInfo ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (CG CGEnv -> State CGInfo ()) -> CG CGEnv -> State CGInfo ()
forall a b. (a -> b) -> a -> b
$ CGEnv -> Bind Var -> CG CGEnv
consCBLet CGEnv
γ' ([(Var, Expr Var)] -> Bind Var
forall b. [(b, Expr b)] -> Bind b
Rec [(Var
x, Expr Var
e')])

cconsE' CGEnv
γ e :: Expr Var
e@(Let b :: Bind Var
b@(NonRec Var
x Expr Var
_) Expr Var
ee) SpecType
t
  = do sp <- (CGInfo -> HashSet Var) -> StateT CGInfo Identity (HashSet Var)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CGInfo -> HashSet Var
specLVars
       if x `S.member` sp
         then cconsLazyLet γ e t
         else do γ' <- consCBLet γ b
                 cconsE γ' ee t

cconsE' CGEnv
γ Expr Var
e (RAllP PVarBV Symbol Symbol (RTypeBV Symbol Symbol RTyCon RTyVar NoReft)
p SpecType
t)
  = CGEnv -> Expr Var -> SpecType -> State CGInfo ()
cconsE CGEnv
γ' Expr Var
e SpecType
t''
  where
    t' :: SpecType
t'         = (UsedPVar,
 (Symbol, [((), Symbol, ExprBV Symbol Symbol)])
 -> ExprBV Symbol Symbol)
-> RReft -> RReft
replacePredsWithRefs (UsedPVar,
 (Symbol, [((), Symbol, ExprBV Symbol Symbol)])
 -> ExprBV Symbol Symbol)
forall {a} {b}.
(UsedPVar,
 (Symbol, [(a, b, ExprBV Symbol Symbol)]) -> ExprBV Symbol Symbol)
su (RReft -> RReft) -> SpecType -> SpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SpecType
t
    su :: (UsedPVar,
 (Symbol, [(a, b, ExprBV Symbol Symbol)]) -> ExprBV Symbol Symbol)
su         = (PVarBV Symbol Symbol (RTypeBV Symbol Symbol RTyCon RTyVar NoReft)
-> UsedPVar
forall v t. PVarV v t -> UsedPVarV v
uPVar PVarBV Symbol Symbol (RTypeBV Symbol Symbol RTyCon RTyVar NoReft)
p, PVarBV Symbol Symbol (RTypeBV Symbol Symbol RTyCon RTyVar NoReft)
-> (Symbol, [(a, b, ExprBV Symbol Symbol)]) -> ExprBV Symbol Symbol
forall t a b.
PVar t
-> (Symbol, [(a, b, ExprBV Symbol Symbol)]) -> ExprBV Symbol Symbol
pVartoRConc PVarBV Symbol Symbol (RTypeBV Symbol Symbol RTyCon RTyVar NoReft)
p)
    ([[(Symbol, SpecType)]]
css, SpecType
t'') = Bool -> SpecType -> ([[(Symbol, SpecType)]], SpecType)
forall c tv r.
TyConable c =>
Bool -> RType c tv r -> ([[(Symbol, RType c tv r)]], RType c tv r)
splitConstraints (Config -> Bool
typeclass (CGEnv -> Config
forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)) SpecType
t'
    γ' :: CGEnv
γ'         = (CGEnv -> [(Symbol, SpecType)] -> CGEnv)
-> CGEnv -> [[(Symbol, SpecType)]] -> CGEnv
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' CGEnv -> [(Symbol, SpecType)] -> CGEnv
addConstraints CGEnv
γ [[(Symbol, SpecType)]]
css

cconsE' CGEnv
γ (Let Bind Var
b Expr Var
e) SpecType
t
  = do γ' <- CGEnv -> Bind Var -> CG CGEnv
consCBLet CGEnv
γ Bind Var
b
       cconsE γ' e t

cconsE' CGEnv
γ (Case Expr Var
e Var
x Type
_ [Alt Var]
cases) SpecType
t
  = do γ' <- CGEnv -> Bind Var -> CG CGEnv
consCBLet CGEnv
γ (Var -> Expr Var -> Bind Var
forall b. b -> Expr b -> Bind b
NonRec Var
x Expr Var
e)
       forM_ cases $ cconsCase γ' x t nonDefAlts
    where
       nonDefAlts :: [AltCon]
nonDefAlts = [AltCon
a | Alt AltCon
a [Var]
_ Expr Var
_ <- [Alt Var]
cases, AltCon
a AltCon -> AltCon -> Bool
forall a. Eq a => a -> a -> Bool
/= AltCon
DEFAULT]
       _msg :: [Char]
_msg = [Char]
"cconsE' #nonDefAlts = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show ([AltCon] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [AltCon]
nonDefAlts)

cconsE' CGEnv
γ (Lam Var
α Expr Var
e) (RAllT RTVar RTyVar (RTypeBV Symbol Symbol RTyCon RTyVar NoReft)
α' SpecType
t RReft
r) | Var -> Bool
isTyVar Var
α
  = do γ' <- CGEnv -> Var -> CG CGEnv
updateEnvironment CGEnv
γ Var
α
       addForAllConstraint γ' α e (RAllT α' t r)
       cconsE γ' e $ subsTyVarMeet' (ty_var_value α', rVar α) t

cconsE' CGEnv
γ (Lam Var
x Expr Var
e) (RFun Symbol
y RFInfo
i SpecType
ty SpecType
t RReft
r)
  | Bool -> Bool
not (Var -> Bool
isTyVar Var
x)
  = do γ' <- CGEnv
γ CGEnv -> ([Char], Symbol, SpecType) -> CG CGEnv
+= ([Char]
"cconsE", Symbol
x', SpecType
ty)
       cconsE γ' e t'
       addFunctionConstraint γ x e (RFun x' i ty t' r')
       addIdA x (AnnDef ty)
  where
    x' :: Symbol
x'  = Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
x
    t' :: SpecType
t'  = SpecType
t SpecType
-> (Variable SpecType,
    ExprBV (Variable SpecType) (Variable SpecType))
-> SpecType
forall a.
Subable a =>
a -> (Variable a, ExprBV (Variable a) (Variable a)) -> a
`F.subst1` (Symbol
Variable SpecType
y, Symbol -> ExprBV Symbol Symbol
forall b v. v -> ExprBV b v
F.EVar Symbol
x')
    r' :: RReft
r'  = RReft
r RReft
-> (Variable RReft, ExprBV (Variable RReft) (Variable RReft))
-> RReft
forall a.
Subable a =>
a -> (Variable a, ExprBV (Variable a) (Variable a)) -> a
`F.subst1` (Symbol
Variable RReft
y, Symbol -> ExprBV Symbol Symbol
forall b v. v -> ExprBV b v
F.EVar Symbol
x')

cconsE' CGEnv
γ (Tick CoreTickish
tt Expr Var
e) SpecType
t
  = CGEnv -> Expr Var -> SpecType -> State CGInfo ()
cconsE (CGEnv
γ CGEnv -> Span -> CGEnv
`setLocation` CoreTickish -> Span
Sp.Tick CoreTickish
tt) Expr Var
e SpecType
t

cconsE' CGEnv
γ (Cast Expr Var
e CoercionR
co) SpecType
t
  -- See Note [Type classes with a single method]
  | Just Expr Var -> Expr Var
f <- CoercionR -> Maybe (Expr Var -> Expr Var)
isClassConCo CoercionR
co
  = CGEnv -> Expr Var -> SpecType -> State CGInfo ()
cconsE CGEnv
γ (Expr Var -> Expr Var
f Expr Var
e) SpecType
t

cconsE' CGEnv
γ e :: Expr Var
e@(Cast Expr Var
e' CoercionR
c) SpecType
t
  = do t' <- (SpecType -> RReft -> SpecType
forall r b v c tv.
Meet r =>
RTypeBV b v c tv r -> r -> RTypeBV b v c tv r
`strengthen` ReftBV Symbol Symbol -> RReft
forall r v. r -> UReftV v r
uTop (SpecType -> ReftBV (ReftBind RReft) (ReftVar RReft)
forall r b v c tv.
(ToReft r, Binder (ReftBind r)) =>
RTypeBV b v c tv r -> ReftBV (ReftBind r) (ReftVar r)
rTypeReft SpecType
t)) (SpecType -> SpecType)
-> StateT CGInfo Identity SpecType
-> StateT CGInfo Identity SpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CGEnv
-> Type -> Expr Var -> CoercionR -> StateT CGInfo Identity SpecType
castTy CGEnv
γ (HasDebugCallStack => Expr Var -> Type
Expr Var -> Type
exprType Expr Var
e) Expr Var
e' CoercionR
c
       addC (SubC γ (F.notracepp ("Casted Type for " ++ GM.showPpr e ++ "\n init type " ++ showpp t) t') t) ("cconsE Cast: " ++ GM.showPpr e)

cconsE' CGEnv
γ Expr Var
e SpecType
t
  = do
       Bool -> State CGInfo () -> State CGInfo ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Config -> Bool
warnOnTermHoles (CGEnv -> Config
forall t. HasConfig t => t -> Config
getConfig CGEnv
γ))  State CGInfo ()
maybeAddHole
       te  <- CGEnv -> Expr Var -> StateT CGInfo Identity SpecType
consE CGEnv
γ Expr Var
e
       te' <- instantiatePreds γ e te >>= addPost γ
       addC (SubC γ te' t) ("cconsE: " ++ "\n t = " ++ showpp t ++ "\n te = " ++ showpp te ++ GM.showPpr e)
  where
    -- See Note [Term holes]
    -- Record the expected type of a direct hole encountered in checking mode.
    maybeAddHole :: State CGInfo ()
maybeAddHole = do
      let isItHole :: Maybe (RealSrcSpan, Var)
isItHole = Expr Var -> Maybe (RealSrcSpan, Var)
detectTypedHole Expr Var
e
      case Maybe (RealSrcSpan, Var)
isItHole of
        Just (RealSrcSpan
srcSpan, Var
x) -> do
          SrcSpan -> Var -> SpecType -> CGEnv -> State CGInfo ()
addHole (RealSrcSpan -> Maybe BufSpan -> SrcSpan
RealSrcSpan RealSrcSpan
srcSpan Maybe BufSpan
forall a. Maybe a
Strict.Nothing) Var
x SpecType
t CGEnv
γ
        Maybe (RealSrcSpan, Var)
_ -> () -> State CGInfo ()
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

lambdaSingleton :: CGEnv -> F.TCEmb TyCon -> Var -> CoreExpr -> CG (UReft F.Reft)
lambdaSingleton :: CGEnv -> TCEmb TyCon -> Var -> Expr Var -> CG RReft
lambdaSingleton CGEnv
γ TCEmb TyCon
tce Var
x Expr Var
e
  | CGEnv -> Bool
forall t. HasConfig t => t -> Bool
higherOrderFlag CGEnv
γ
  = do expr <- CGEnv -> Expr Var -> CG (Maybe (ExprBV Symbol Symbol))
lamExpr CGEnv
γ Expr Var
e
       return $ case expr of
         Just ExprBV Symbol Symbol
e' -> ReftBV Symbol Symbol -> RReft
forall r v. r -> UReftV v r
uTop (ReftBV Symbol Symbol -> RReft) -> ReftBV Symbol Symbol -> RReft
forall a b. (a -> b) -> a -> b
$ ExprBV Symbol Symbol -> ReftBV Symbol Symbol
forall a. Expression a => a -> ReftBV Symbol Symbol
F.exprReft (ExprBV Symbol Symbol -> ReftBV Symbol Symbol)
-> ExprBV Symbol Symbol -> ReftBV Symbol Symbol
forall a b. (a -> b) -> a -> b
$ (Symbol, Sort) -> ExprBV Symbol Symbol -> ExprBV Symbol Symbol
forall b v. (b, Sort) -> ExprBV b v -> ExprBV b v
F.ELam (Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
x, Sort
sx) ExprBV Symbol Symbol
e'
         Maybe (ExprBV Symbol Symbol)
_       -> RReft
forall a. Monoid a => a
mempty
  where
    sx :: Sort
sx = TCEmb TyCon -> Type -> Sort
typeSort TCEmb TyCon
tce (Type -> Sort) -> Type -> Sort
forall a b. (a -> b) -> a -> b
$ Type -> Type
Ghc.expandTypeSynonyms (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Var -> Type
varType Var
x
lambdaSingleton CGEnv
_ TCEmb TyCon
_ Var
_ Expr Var
_
  = RReft -> CG RReft
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return RReft
forall a. Monoid a => a
mempty

addForAllConstraint :: CGEnv -> Var -> CoreExpr -> SpecType -> CG ()
addForAllConstraint :: CGEnv -> Var -> Expr Var -> SpecType -> State CGInfo ()
addForAllConstraint CGEnv
γ Var
_ Expr Var
_ (RAllT RTVar RTyVar (RTypeBV Symbol Symbol RTyCon RTyVar NoReft)
rtv SpecType
rt RReft
rr)
  | RReft -> Bool
forall r. ToReft r => r -> Bool
isTauto RReft
rr
  = () -> State CGInfo ()
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  | Bool
otherwise
  = do t'       <- Bool -> SpecType -> StateT CGInfo Identity SpecType
forall (m :: * -> *) a. Freshable m a => Bool -> a -> m a
true (Config -> Bool
typeclass (CGEnv -> Config
forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)) SpecType
rt
       let truet = RTVar RTyVar (RTypeBV Symbol Symbol RTyCon RTyVar NoReft)
-> SpecType -> RReft -> SpecType
forall b v c tv r.
RTVUBV b v c tv -> RTypeBV b v c tv r -> r -> RTypeBV b v c tv r
RAllT RTVar RTyVar (RTypeBV Symbol Symbol RTyCon RTyVar NoReft)
rtv (SpecType -> RReft -> SpecType) -> SpecType -> RReft -> SpecType
forall a b. (a -> b) -> a -> b
$ SpecType -> SpecType
forall b v c tv r. RTypeBV b v c tv r -> RTypeBV b v c tv r
unRAllP SpecType
t'
       addC (SubC γ (truet mempty) $ truet rr) "forall constraint true"
  where unRAllP :: RTypeBV b v c tv r -> RTypeBV b v c tv r
unRAllP (RAllT RTVUBV b v c tv
a RTypeBV b v c tv r
t r
r) = RTVUBV b v c tv -> RTypeBV b v c tv r -> r -> RTypeBV b v c tv r
forall b v c tv r.
RTVUBV b v c tv -> RTypeBV b v c tv r -> r -> RTypeBV b v c tv r
RAllT RTVUBV b v c tv
a (RTypeBV b v c tv r -> RTypeBV b v c tv r
unRAllP RTypeBV b v c tv r
t) r
r
        unRAllP (RAllP PVUBV b v c tv
_ RTypeBV b v c tv r
t)   = RTypeBV b v c tv r -> RTypeBV b v c tv r
unRAllP RTypeBV b v c tv r
t
        unRAllP RTypeBV b v c tv r
t             = RTypeBV b v c tv r
t
addForAllConstraint CGEnv
γ Var
_ Expr Var
_ SpecType
_
  = Maybe SrcSpan -> [Char] -> State CGInfo ()
forall a. Maybe SrcSpan -> [Char] -> a
impossible (SrcSpan -> Maybe SrcSpan
forall a. a -> Maybe a
Just (SrcSpan -> Maybe SrcSpan) -> SrcSpan -> Maybe SrcSpan
forall a b. (a -> b) -> a -> b
$ CGEnv -> SrcSpan
getLocation CGEnv
γ) [Char]
"addFunctionConstraint: called on non function argument"


addFunctionConstraint :: CGEnv -> Var -> CoreExpr -> SpecType -> CG ()
addFunctionConstraint :: CGEnv -> Var -> Expr Var -> SpecType -> State CGInfo ()
addFunctionConstraint CGEnv
γ Var
x Expr Var
e (RFun Symbol
y RFInfo
i SpecType
ty SpecType
t RReft
r)
  = do ty'      <- Bool -> SpecType -> StateT CGInfo Identity SpecType
forall (m :: * -> *) a. Freshable m a => Bool -> a -> m a
true (Config -> Bool
typeclass (CGEnv -> Config
forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)) SpecType
ty
       t'       <- true (typeclass (getConfig γ)) t
       let truet = Symbol -> RFInfo -> SpecType -> SpecType -> RReft -> SpecType
forall b v c tv r.
b
-> RFInfo
-> RTypeBV b v c tv r
-> RTypeBV b v c tv r
-> r
-> RTypeBV b v c tv r
RFun Symbol
y RFInfo
i SpecType
ty' SpecType
t'
       lamE <- lamExpr γ e
       case (lamE, higherOrderFlag γ) of
          (Just ExprBV Symbol Symbol
e', Bool
True) -> do tce    <- (CGInfo -> TCEmb TyCon) -> StateT CGInfo Identity (TCEmb TyCon)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CGInfo -> TCEmb TyCon
tyConEmbed
                                let sx  = TCEmb TyCon -> Type -> Sort
typeSort TCEmb TyCon
tce (Type -> Sort) -> Type -> Sort
forall a b. (a -> b) -> a -> b
$ Var -> Type
varType Var
x
                                let ref = ReftBV Symbol Symbol -> UReftV v (ReftBV Symbol Symbol)
forall r v. r -> UReftV v r
uTop (ReftBV Symbol Symbol -> UReftV v (ReftBV Symbol Symbol))
-> ReftBV Symbol Symbol -> UReftV v (ReftBV Symbol Symbol)
forall a b. (a -> b) -> a -> b
$ ExprBV Symbol Symbol -> ReftBV Symbol Symbol
forall a. Expression a => a -> ReftBV Symbol Symbol
F.exprReft (ExprBV Symbol Symbol -> ReftBV Symbol Symbol)
-> ExprBV Symbol Symbol -> ReftBV Symbol Symbol
forall a b. (a -> b) -> a -> b
$ (Symbol, Sort) -> ExprBV Symbol Symbol -> ExprBV Symbol Symbol
forall b v. (b, Sort) -> ExprBV b v -> ExprBV b v
F.ELam (Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
x, Sort
sx) ExprBV Symbol Symbol
e'
                                addC (SubC γ (truet ref) $ truet r) "function constraint singleton"
          (Maybe (ExprBV Symbol Symbol), Bool)
_ -> SubC -> [Char] -> State CGInfo ()
addC (CGEnv -> SpecType -> SpecType -> SubC
SubC CGEnv
γ (RReft -> SpecType
truet RReft
forall a. Monoid a => a
mempty) (SpecType -> SubC) -> SpecType -> SubC
forall a b. (a -> b) -> a -> b
$ RReft -> SpecType
truet RReft
r) [Char]
"function constraint true"
addFunctionConstraint CGEnv
γ Var
_ Expr Var
_ SpecType
_
  = Maybe SrcSpan -> [Char] -> State CGInfo ()
forall a. Maybe SrcSpan -> [Char] -> a
impossible (SrcSpan -> Maybe SrcSpan
forall a. a -> Maybe a
Just (SrcSpan -> Maybe SrcSpan) -> SrcSpan -> Maybe SrcSpan
forall a b. (a -> b) -> a -> b
$ CGEnv -> SrcSpan
getLocation CGEnv
γ) [Char]
"addFunctionConstraint: called on non function argument"

splitConstraints :: TyConable c
                 => Bool -> RType c tv r -> ([[(F.Symbol, RType c tv r)]], RType c tv r)
splitConstraints :: forall c tv r.
TyConable c =>
Bool -> RType c tv r -> ([[(Symbol, RType c tv r)]], RType c tv r)
splitConstraints Bool
allowTC (RRTy [(Symbol, RTypeBV Symbol Symbol c tv r)]
cs r
_ Oblig
OCons RTypeBV Symbol Symbol c tv r
t)
  = let ([[(Symbol, RTypeBV Symbol Symbol c tv r)]]
css, RTypeBV Symbol Symbol c tv r
t') = Bool
-> RTypeBV Symbol Symbol c tv r
-> ([[(Symbol, RTypeBV Symbol Symbol c tv r)]],
    RTypeBV Symbol Symbol c tv r)
forall c tv r.
TyConable c =>
Bool -> RType c tv r -> ([[(Symbol, RType c tv r)]], RType c tv r)
splitConstraints Bool
allowTC RTypeBV Symbol Symbol c tv r
t in ([(Symbol, RTypeBV Symbol Symbol c tv r)]
cs[(Symbol, RTypeBV Symbol Symbol c tv r)]
-> [[(Symbol, RTypeBV Symbol Symbol c tv r)]]
-> [[(Symbol, RTypeBV Symbol Symbol c tv r)]]
forall a. a -> [a] -> [a]
:[[(Symbol, RTypeBV Symbol Symbol c tv r)]]
css, RTypeBV Symbol Symbol c tv r
t')
splitConstraints Bool
allowTC (RFun Symbol
x RFInfo
i tx :: RTypeBV Symbol Symbol c tv r
tx@(RApp c
c [RTypeBV Symbol Symbol c tv r]
_ [RTPropBV Symbol Symbol c tv r]
_ r
_) RTypeBV Symbol Symbol c tv r
t r
r) | c -> Bool
forall {c}. TyConable c => c -> Bool
isErasable c
c
  = let ([[(Symbol, RTypeBV Symbol Symbol c tv r)]]
css, RTypeBV Symbol Symbol c tv r
t') = Bool
-> RTypeBV Symbol Symbol c tv r
-> ([[(Symbol, RTypeBV Symbol Symbol c tv r)]],
    RTypeBV Symbol Symbol c tv r)
forall c tv r.
TyConable c =>
Bool -> RType c tv r -> ([[(Symbol, RType c tv r)]], RType c tv r)
splitConstraints Bool
allowTC  RTypeBV Symbol Symbol c tv r
t in ([[(Symbol, RTypeBV Symbol Symbol c tv r)]]
css, Symbol
-> RFInfo
-> RTypeBV Symbol Symbol c tv r
-> RTypeBV Symbol Symbol c tv r
-> r
-> RTypeBV Symbol Symbol c tv r
forall b v c tv r.
b
-> RFInfo
-> RTypeBV b v c tv r
-> RTypeBV b v c tv r
-> r
-> RTypeBV b v c tv r
RFun Symbol
x RFInfo
i RTypeBV Symbol Symbol c tv r
tx RTypeBV Symbol Symbol c tv r
t' r
r)
  where isErasable :: c -> Bool
isErasable = if Bool
allowTC then c -> Bool
forall {c}. TyConable c => c -> Bool
isEmbeddedDict else c -> Bool
forall {c}. TyConable c => c -> Bool
isClass
splitConstraints Bool
_ RTypeBV Symbol Symbol c tv r
t
  = ([], RTypeBV Symbol Symbol c tv r
t)

-------------------------------------------------------------------
-- | @instantiatePreds@ peels away the universally quantified @PVars@
--   of a @RType@, generates fresh @Ref@ for them and substitutes them
--   in the body.
-------------------------------------------------------------------
instantiatePreds :: CGEnv
                 -> CoreExpr
                 -> SpecType
                 -> CG SpecType
instantiatePreds :: CGEnv -> Expr Var -> SpecType -> StateT CGInfo Identity SpecType
instantiatePreds CGEnv
γ Expr Var
e (RAllP PVarBV Symbol Symbol (RTypeBV Symbol Symbol RTyCon RTyVar NoReft)
π SpecType
t)
  = do r <- CGEnv
-> Expr Var
-> PVarBV
     Symbol Symbol (RTypeBV Symbol Symbol RTyCon RTyVar NoReft)
-> CG (RTProp RTyCon RTyVar RReft)
freshPredRef CGEnv
γ Expr Var
e PVarBV Symbol Symbol (RTypeBV Symbol Symbol RTyCon RTyVar NoReft)
π
       instantiatePreds γ e $ replacePreds "consE" t [(π, r)]

instantiatePreds CGEnv
_ Expr Var
_ SpecType
t0
  = SpecType -> StateT CGInfo Identity SpecType
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return SpecType
t0


-------------------------------------------------------------------
cconsLazyLet :: CGEnv
             -> CoreExpr
             -> SpecType
             -> CG ()
cconsLazyLet :: CGEnv -> Expr Var -> SpecType -> State CGInfo ()
cconsLazyLet CGEnv
γ (Let (NonRec Var
x Expr Var
ex) Expr Var
e) SpecType
t
  = do tx <- Bool -> Type -> StateT CGInfo Identity SpecType
trueTy (Config -> Bool
typeclass (CGEnv -> Config
forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)) (Var -> Type
varType Var
x)
       γ' <- (γ, "Let NonRec") +++= (F.symbol x, ex, tx)
       cconsE γ' e t
cconsLazyLet CGEnv
_ Expr Var
_ SpecType
_
  = Maybe SrcSpan -> [Char] -> State CGInfo ()
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing [Char]
"Constraint.Generate.cconsLazyLet called on invalid inputs"


---------------------------------------------------------
-- | Bidirectional Constraint Generation: SYNTHESIS ----------------------------
--------------------------------------------------------------------------------
consE :: CGEnv -> CoreExpr -> CG SpecType
--------------------------------------------------------------------------------
consE :: CGEnv -> Expr Var -> StateT CGInfo Identity SpecType
consE CGEnv
γ Expr Var
e
  | CGEnv -> Bool
forall t. HasConfig t => t -> Bool
patternFlag CGEnv
γ
  , Just Pattern
p <- Expr Var -> Maybe Pattern
Rs.lift Expr Var
e
  = CGEnv -> Pattern -> Type -> StateT CGInfo Identity SpecType
consPattern CGEnv
γ ([Char] -> Pattern -> Pattern
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"CONSE-PATTERN: " Pattern
p) (HasDebugCallStack => Expr Var -> Type
Expr Var -> Type
exprType Expr Var
e)

-- NV CHECK 3 (unVar and does this hack even needed?)
-- NV (below) is a hack to type polymorphic axiomatized functions
-- no need to check this code with flag, the axioms environment with
-- is empty if there is no axiomatization.

-- [NOTE: PLE-OPT] We *disable* refined instantiation for
-- reflected functions inside proofs.

-- If datacon definitions have references to self for fancy termination,
-- ignore them at the construction.
consE CGEnv
γ (Var Var
x) | Var -> Bool
GM.isDataConId Var
x
  = do t0 <- HasCallStack => CGEnv -> Var -> StateT CGInfo Identity SpecType
CGEnv -> Var -> StateT CGInfo Identity SpecType
varRefType CGEnv
γ Var
x
       -- NV: The check is expected to fail most times, so
       --     it is cheaper than direclty fmap ignoreSelf.
       let hasSelf = Symbol
selfSymbol Symbol -> [Symbol] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` SpecType -> [Variable SpecType]
forall a. Subable a => a -> [Variable a]
F.syms SpecType
t0
       let t = if Bool
hasSelf
                then (ReftBV Symbol Symbol -> ReftBV Symbol Symbol) -> RReft -> RReft
forall a b.
(a -> b) -> UReftBV Symbol Symbol a -> UReftBV Symbol Symbol b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ReftBV Symbol Symbol -> ReftBV Symbol Symbol
ignoreSelf (RReft -> RReft) -> SpecType -> SpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SpecType
t0
                else SpecType
t0
       addLocA (Just x) (getLocation γ) (varAnn γ x t)
       return t

consE CGEnv
γ (Var Var
x)
  = do t <- HasCallStack => CGEnv -> Var -> StateT CGInfo Identity SpecType
CGEnv -> Var -> StateT CGInfo Identity SpecType
varRefType CGEnv
γ Var
x
       addLocA (Just x) (getLocation γ) (varAnn γ x t)
       return t

consE CGEnv
_ (Lit Literal
c)
  = SpecType -> StateT CGInfo Identity SpecType
forall (m :: * -> *). FreshM m => SpecType -> m SpecType
refreshVV (SpecType -> StateT CGInfo Identity SpecType)
-> SpecType -> StateT CGInfo Identity SpecType
forall a b. (a -> b) -> a -> b
$ RType RTyCon RTyVar (ReftBV Symbol Symbol) -> SpecType
forall c tv a. RType c tv a -> RType c tv (UReft a)
uRType (RType RTyCon RTyVar (ReftBV Symbol Symbol) -> SpecType)
-> RType RTyCon RTyVar (ReftBV Symbol Symbol) -> SpecType
forall a b. (a -> b) -> a -> b
$ Literal -> RType RTyCon RTyVar (ReftBV Symbol Symbol)
literalFRefType Literal
c

consE CGEnv
γ e' :: Expr Var
e'@(App Expr Var
_ Expr Var
_) =
  do
    t <- if Config -> Bool
warnOnTermHoles (CGEnv -> Config
forall t. HasConfig t => t -> Config
getConfig CGEnv
γ) then StateT CGInfo Identity SpecType
synthesizeWithHole else CGEnv -> Expr Var -> StateT CGInfo Identity SpecType
consEApp CGEnv
γ Expr Var
e'
    checkANFHoleInExpr e' t
    return t
  where
    -- See Note [Term holes]
    -- Record the synthesized type of a direct hole encountered in synthesis
    -- mode before the caller consumes it.
    synthesizeWithHole :: StateT CGInfo Identity SpecType
synthesizeWithHole = do
      let isItHole :: Maybe (RealSrcSpan, Var)
isItHole = Expr Var -> Maybe (RealSrcSpan, Var)
detectTypedHole Expr Var
e'
      t <- CGEnv -> Expr Var -> StateT CGInfo Identity SpecType
consEApp CGEnv
γ Expr Var
e'
      _ <- case isItHole of
        Just (RealSrcSpan
srcSpan, Var
x) -> do
          SrcSpan -> Var -> SpecType -> CGEnv -> State CGInfo ()
addHole (RealSrcSpan -> Maybe BufSpan -> SrcSpan
RealSrcSpan RealSrcSpan
srcSpan Maybe BufSpan
forall a. Maybe a
Strict.Nothing) Var
x SpecType
t CGEnv
γ
        Maybe (RealSrcSpan, Var)
_ -> () -> State CGInfo ()
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      return t
consE CGEnv
γ (Lam Var
α Expr Var
e) | Var -> Bool
isTyVar Var
α
  = do γ' <- CGEnv -> Var -> CG CGEnv
updateEnvironment CGEnv
γ Var
α
       t' <- consE γ' e
       return $ RAllT (makeRTVar $ rTyVar α) t' mempty

consE CGEnv
γ  e :: Expr Var
e@(Lam Var
x Expr Var
e1)
  = do tx      <- Bool
-> KVKind -> Expr Var -> Type -> StateT CGInfo Identity SpecType
freshTyType (Config -> Bool
typeclass (CGEnv -> Config
forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)) KVKind
LamE (Var -> Expr Var
forall b. Var -> Expr b
Var Var
x) Type
τx
       γ'      <- γ += ("consE", F.symbol x, tx)
       t1      <- consE γ' e1
       addIdA x $ AnnDef tx
       addW     $ WfC γ tx
       tce     <- gets tyConEmbed
       lamSing <- lambdaSingleton γ tce x e1
       return   $ RFun (F.symbol x) (mkRFInfo $ getConfig γ) tx t1 lamSing
    where
      FunTy { ft_arg :: Type -> Type
ft_arg = Type
τx } = HasDebugCallStack => Expr Var -> Type
Expr Var -> Type
exprType Expr Var
e

consE CGEnv
γ e :: Expr Var
e@(Let Bind Var
_ Expr Var
_)
  = KVKind -> CGEnv -> Expr Var -> StateT CGInfo Identity SpecType
cconsFreshE KVKind
LetE CGEnv
γ Expr Var
e

consE CGEnv
γ e :: Expr Var
e@(Case Expr Var
_ Var
_ Type
_ [Alt Var
_])
  | Just p :: Pattern
p@Rs.PatProject{} <- Expr Var -> Maybe Pattern
Rs.lift Expr Var
e
  = CGEnv -> Pattern -> Type -> StateT CGInfo Identity SpecType
consPattern CGEnv
γ Pattern
p (HasDebugCallStack => Expr Var -> Type
Expr Var -> Type
exprType Expr Var
e)

consE CGEnv
γ e :: Expr Var
e@(Case Expr Var
_ Var
_ Type
_ [Alt Var]
cs)
  = KVKind -> CGEnv -> Expr Var -> StateT CGInfo Identity SpecType
cconsFreshE ([Alt Var] -> KVKind
caseKVKind [Alt Var]
cs) CGEnv
γ Expr Var
e

consE CGEnv
γ (Tick CoreTickish
tt Expr Var
e)
  = do t <- CGEnv -> Expr Var -> StateT CGInfo Identity SpecType
consE (CGEnv -> Span -> CGEnv
setLocation CGEnv
γ (CoreTickish -> Span
Sp.Tick CoreTickish
tt)) Expr Var
e
       addLocA Nothing (GM.tickSrcSpan tt) (AnnUse t)
       return t

-- See Note [Type classes with a single method]
consE CGEnv
γ (Cast Expr Var
e CoercionR
co)
  | Just Expr Var -> Expr Var
f <- CoercionR -> Maybe (Expr Var -> Expr Var)
isClassConCo CoercionR
co
  = CGEnv -> Expr Var -> StateT CGInfo Identity SpecType
consE CGEnv
γ (Expr Var -> Expr Var
f Expr Var
e)

consE CGEnv
γ e :: Expr Var
e@(Cast Expr Var
e' CoercionR
c)
  = CGEnv
-> Type -> Expr Var -> CoercionR -> StateT CGInfo Identity SpecType
castTy CGEnv
γ (HasDebugCallStack => Expr Var -> Type
Expr Var -> Type
exprType Expr Var
e) Expr Var
e' CoercionR
c

consE CGEnv
γ e :: Expr Var
e@(Coercion CoercionR
_)
   = Bool -> Type -> StateT CGInfo Identity SpecType
trueTy (Config -> Bool
typeclass (CGEnv -> Config
forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)) (Type -> StateT CGInfo Identity SpecType)
-> Type -> StateT CGInfo Identity SpecType
forall a b. (a -> b) -> a -> b
$ HasDebugCallStack => Expr Var -> Type
Expr Var -> Type
exprType Expr Var
e

consE CGEnv
_ e :: Expr Var
e@(Type Type
t)
  = Maybe SrcSpan -> [Char] -> StateT CGInfo Identity SpecType
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing ([Char] -> StateT CGInfo Identity SpecType)
-> [Char] -> StateT CGInfo Identity SpecType
forall a b. (a -> b) -> a -> b
$ [Char]
"consE cannot handle type " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (Expr Var, Type) -> [Char]
forall a. Outputable a => a -> [Char]
GM.showPpr (Expr Var
e, Type
t)

-- | Attach the current expression and inferred type to any ANF binders that
--   were previously recognized as naming a term hole. This compensates for ANF
--   normalization, which often moves the informative constraints from the hole
--   occurrence onto the fresh binder that stands for it.
--
-- See Note [Term holes]
checkANFHoleInExpr :: CoreExpr -> SpecType -> CG ()
checkANFHoleInExpr :: Expr Var -> SpecType -> State CGInfo ()
checkANFHoleInExpr Expr Var
e SpecType
t = do
  let vars :: [Var]
vars = Expr Var -> [Var]
collectVars Expr Var
e
  [Var] -> (Var -> State CGInfo ()) -> State CGInfo ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Var]
vars ((Var -> State CGInfo ()) -> State CGInfo ())
-> (Var -> State CGInfo ()) -> State CGInfo ()
forall a b. (a -> b) -> a -> b
$ \Var
var -> do
    isANF <- Var -> CG (Maybe (Var, SrcSpan))
isANFInHole Var
var
    case isANF of
      Just (Var, SrcSpan)
uniqueVar -> (Var, SrcSpan) -> Var -> Expr Var -> SpecType -> State CGInfo ()
addHoleANF (Var, SrcSpan)
uniqueVar Var
var Expr Var
e SpecType
t
      Maybe (Var, SrcSpan)
_ -> () -> State CGInfo ()
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
-- | Collect every variable mentioned in a Core expression so
--   'checkANFHoleInExpr' can look for ANF binders linked to a hole.
collectVars :: CoreExpr -> [Var]
collectVars :: Expr Var -> [Var]
collectVars (Var Var
x) = [Var
x]
collectVars (App Expr Var
e1 Expr Var
e2) = Expr Var -> [Var]
collectVars Expr Var
e1 [Var] -> [Var] -> [Var]
forall a. [a] -> [a] -> [a]
++ Expr Var -> [Var]
collectVars Expr Var
e2
collectVars (Lam Var
x Expr Var
e) = Var
x Var -> [Var] -> [Var]
forall a. a -> [a] -> [a]
: Expr Var -> [Var]
collectVars Expr Var
e
collectVars (Let (NonRec Var
x Expr Var
e1) Expr Var
e2) = Var
x Var -> [Var] -> [Var]
forall a. a -> [a] -> [a]
: Expr Var -> [Var]
collectVars Expr Var
e1 [Var] -> [Var] -> [Var]
forall a. [a] -> [a] -> [a]
++ Expr Var -> [Var]
collectVars Expr Var
e2
collectVars (Let (Rec [(Var, Expr Var)]
xes) Expr Var
e) =
  let ([Var]
xs, [Expr Var]
es) = [(Var, Expr Var)] -> ([Var], [Expr Var])
forall a b. [(a, b)] -> ([a], [b])
unzip [(Var, Expr Var)]
xes
  in [Var]
xs [Var] -> [Var] -> [Var]
forall a. [a] -> [a] -> [a]
++ (Expr Var -> [Var]) -> [Expr Var] -> [Var]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Expr Var -> [Var]
collectVars [Expr Var]
es [Var] -> [Var] -> [Var]
forall a. [a] -> [a] -> [a]
++ Expr Var -> [Var]
collectVars Expr Var
e
collectVars (Case Expr Var
e Var
x Type
_ [Alt Var]
alts) =
  Var
x Var -> [Var] -> [Var]
forall a. a -> [a] -> [a]
: Expr Var -> [Var]
collectVars Expr Var
e [Var] -> [Var] -> [Var]
forall a. [a] -> [a] -> [a]
++ (Alt Var -> [Var]) -> [Alt Var] -> [Var]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Alt Var -> [Var]
collectAltVars [Alt Var]
alts
  where collectAltVars :: Alt Var -> [Var]
collectAltVars (Alt AltCon
_ [Var]
xs Expr Var
e') = [Var]
xs [Var] -> [Var] -> [Var]
forall a. [a] -> [a] -> [a]
++ Expr Var -> [Var]
collectVars Expr Var
e'
collectVars Expr Var
_ = []

consEApp :: CGEnv -> CoreExpr -> CG SpecType
consEApp :: CGEnv -> Expr Var -> StateT CGInfo Identity SpecType
consEApp CGEnv
γ e' :: Expr Var
e'@(App Expr Var
e a :: Expr Var
a@(Type Type
τ))
  = do
       RAllT α te _ <- ([Char], Expr Var) -> CGEnv -> SpecType -> SpecType
forall a.
Outputable a =>
([Char], a) -> CGEnv -> SpecType -> SpecType
checkAll ([Char]
"Non-all TyApp with expr", Expr Var
e) CGEnv
γ (SpecType -> SpecType)
-> StateT CGInfo Identity SpecType
-> StateT CGInfo Identity SpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CGEnv -> Expr Var -> StateT CGInfo Identity SpecType
consE CGEnv
γ Expr Var
e
       t            <- if not (nopolyinfer (getConfig γ)) && isPos α && isGenericVar (ty_var_value α) te
                         then freshTyType (typeclass (getConfig γ)) TypeInstE e τ
                         else trueTy (typeclass (getConfig γ)) τ
       addW          $ WfC γ t
       t'           <- refreshVV t
       tt0          <- instantiatePreds γ e' (subsTyVarMeet' (ty_var_value α, t') te)
       let tyVarSym  = RTyVar -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (RTVar RTyVar (RTypeBV Symbol Symbol RTyCon RTyVar NoReft) -> RTyVar
forall tv s. RTVar tv s -> tv
ty_var_value RTVar RTyVar (RTypeBV Symbol Symbol RTyCon RTyVar NoReft)
α)
           tyVarSort = TCEmb TyCon -> Type -> Sort
typeSort (CGEnv -> TCEmb TyCon
emb CGEnv
γ) (Type -> Type
Ghc.expandTypeSynonyms Type
τ)
           tt0'      = Symbol -> Sort -> SpecType -> SpecType
addTyVarSubToKVars Symbol
tyVarSym Sort
tyVarSort SpecType
tt0
           tt        = CGEnv -> Expr Var -> SpecType -> SpecType
makeSingleton CGEnv
γ (Expr Var -> Expr Var
simplify Expr Var
e') (SpecType -> SpecType) -> SpecType -> SpecType
forall a b. (a -> b) -> a -> b
$ CGEnv -> RTyVar -> Type -> SpecType -> SpecType
subsTyReft CGEnv
γ (RTVar RTyVar (RTypeBV Symbol Symbol RTyCon RTyVar NoReft) -> RTyVar
forall tv s. RTVar tv s -> tv
ty_var_value RTVar RTyVar (RTypeBV Symbol Symbol RTyCon RTyVar NoReft)
α) Type
τ SpecType
tt0'
       return $ case rTVarToBind α of
         Just (Symbol
x, RTypeBV Symbol Symbol RTyCon RTyVar NoReft
_) -> SpecType
-> (ExprBV Symbol Symbol -> SpecType)
-> Maybe (ExprBV Symbol Symbol)
-> SpecType
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (CGEnv -> Expr Var -> Symbol -> SpecType -> Expr Var -> SpecType
forall a a2.
(Show a, Show a2, Subable a, Variable a ~ Symbol) =>
CGEnv -> Expr Var -> Symbol -> a -> a2 -> a
checkUnbound CGEnv
γ Expr Var
e' Symbol
x SpecType
tt Expr Var
a) (SpecType
-> (Variable SpecType,
    ExprBV (Variable SpecType) (Variable SpecType))
-> SpecType
forall a.
Subable a =>
a -> (Variable a, ExprBV (Variable a) (Variable a)) -> a
F.subst1 SpecType
tt ((Symbol, ExprBV Symbol Symbol) -> SpecType)
-> (ExprBV Symbol Symbol -> (Symbol, ExprBV Symbol Symbol))
-> ExprBV Symbol Symbol
-> SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol
x,)) (Type -> Maybe (ExprBV Symbol Symbol)
argType Type
τ)
         Maybe (Symbol, RTypeBV Symbol Symbol RTyCon RTyVar NoReft)
Nothing     -> SpecType
tt
  where
    isPos :: RTVar tv s -> Bool
isPos RTVar tv s
α = Bool -> Bool
not (Config -> Bool
extensionality (CGEnv -> Config
forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)) Bool -> Bool -> Bool
|| RTVInfo s -> Bool
forall s. RTVInfo s -> Bool
rtv_is_pol (RTVar tv s -> RTVInfo s
forall tv s. RTVar tv s -> RTVInfo s
ty_var_info RTVar tv s
α)

consEApp CGEnv
γ e' :: Expr Var
e'@(App Expr Var
e Expr Var
a) | Just Var
aDict <- CGEnv -> Expr Var -> Maybe Var
getExprDict CGEnv
γ Expr Var
a
  = case Maybe (HashMap Symbol (RISig SpecType))
-> Var -> Maybe (RISig SpecType)
forall a1 a.
(Symbolic a1, Show a) =>
Maybe (HashMap Symbol a) -> a1 -> Maybe a
dhasinfo (DEnv Var SpecType -> Var -> Maybe (HashMap Symbol (RISig SpecType))
forall k t.
(Eq k, Hashable k) =>
DEnv k t -> k -> Maybe (HashMap Symbol (RISig t))
dlookup (CGEnv -> DEnv Var SpecType
denv CGEnv
γ) Var
aDict) (CGEnv -> Expr Var -> Var
getExprFun CGEnv
γ Expr Var
e) of
      Just RISig SpecType
riSig -> SpecType -> StateT CGInfo Identity SpecType
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (SpecType -> StateT CGInfo Identity SpecType)
-> SpecType -> StateT CGInfo Identity SpecType
forall a b. (a -> b) -> a -> b
$ RISig SpecType -> SpecType
forall a. RISig a -> a
fromRISig RISig SpecType
riSig
      Maybe (RISig SpecType)
_          -> do
        ([], πs, te) <- SpecType
-> ([(RTVar RTyVar (RTypeBV Symbol Symbol RTyCon RTyVar NoReft),
      RReft)],
    [PVarBV
       Symbol Symbol (RTypeBV Symbol Symbol RTyCon RTyVar NoReft)],
    SpecType)
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 (SpecType
 -> ([(RTVar RTyVar (RTypeBV Symbol Symbol RTyCon RTyVar NoReft),
       RReft)],
     [PVarBV
        Symbol Symbol (RTypeBV Symbol Symbol RTyCon RTyVar NoReft)],
     SpecType))
-> StateT CGInfo Identity SpecType
-> StateT
     CGInfo
     Identity
     ([(RTVar RTyVar (RTypeBV Symbol Symbol RTyCon RTyVar NoReft),
        RReft)],
      [PVarBV
         Symbol Symbol (RTypeBV Symbol Symbol RTyCon RTyVar NoReft)],
      SpecType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CGEnv -> Expr Var -> StateT CGInfo Identity SpecType
consE CGEnv
γ Expr Var
e
        te'          <- instantiatePreds γ e' $ foldr RAllP te πs
        (γ', te''')  <- dropExists γ te'
        te''         <- dropConstraints γ te'''
        updateLocA {- πs -} (exprLoc e) te''
        let RFun x _ tx t _ = checkFun ("Non-fun App with caller ", e') γ te''
        cconsE γ' a tx
        addPost γ'        $ maybe (checkUnbound γ' e' x t a) (F.subst1 t . (x,)) (argExpr γ a)

consEApp CGEnv
γ e' :: Expr Var
e'@(App Expr Var
e Expr Var
a)
  = do ([], πs, te) <- SpecType
-> ([(RTVar RTyVar (RTypeBV Symbol Symbol RTyCon RTyVar NoReft),
      RReft)],
    [PVarBV
       Symbol Symbol (RTypeBV Symbol Symbol RTyCon RTyVar NoReft)],
    SpecType)
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 (SpecType
 -> ([(RTVar RTyVar (RTypeBV Symbol Symbol RTyCon RTyVar NoReft),
       RReft)],
     [PVarBV
        Symbol Symbol (RTypeBV Symbol Symbol RTyCon RTyVar NoReft)],
     SpecType))
-> StateT CGInfo Identity SpecType
-> StateT
     CGInfo
     Identity
     ([(RTVar RTyVar (RTypeBV Symbol Symbol RTyCon RTyVar NoReft),
        RReft)],
      [PVarBV
         Symbol Symbol (RTypeBV Symbol Symbol RTyCon RTyVar NoReft)],
      SpecType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CGEnv -> Expr Var -> StateT CGInfo Identity SpecType
consE CGEnv
γ {- GM.tracePpr ("APP-EXPR: " ++ GM.showPpr (exprType e)) -} Expr Var
e
       te1        <- instantiatePreds γ e' $ foldr RAllP te πs
       (γ', te2)  <- dropExists γ te1
       te3        <- dropConstraints γ te2
       updateLocA (exprLoc e) te3
       let RFun x _ tx t _ = checkFun ("Non-fun App with caller ", e') γ te3
       cconsE γ' a tx
       makeSingleton γ' (simplify e') <$> addPost γ' (maybe (checkUnbound γ' e' x t a) (F.subst1 t . (x,)) (argExpr γ $ simplify a))
consEApp CGEnv
_ Expr Var
_ = Maybe SrcSpan -> [Char] -> StateT CGInfo Identity SpecType
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing [Char]
"Constraint.Generate.consEApp called on invalid inputs"

caseKVKind ::[Alt Var] -> KVKind
caseKVKind :: [Alt Var] -> KVKind
caseKVKind [Alt (DataAlt DataCon
_) [Var]
_ (Var Var
_)] = KVKind
ProjectE
caseKVKind [Alt Var]
cs                          = Int -> KVKind
CaseE ([Alt Var] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Alt Var]
cs)

updateEnvironment :: CGEnv  -> TyVar -> CG CGEnv
updateEnvironment :: CGEnv -> Var -> CG CGEnv
updateEnvironment CGEnv
γ Var
a
  | Type -> Bool
isValKind (Var -> Type
tyVarKind Var
a)
  = CGEnv
γ CGEnv -> ([Char], Symbol, SpecType) -> CG CGEnv
+= ([Char]
"varType", Name -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (Name -> Symbol) -> Name -> Symbol
forall a b. (a -> b) -> a -> b
$ Var -> Name
varName Var
a, Type -> SpecType
forall r. IsReft r => Type -> RRType r
kindToRType (Type -> SpecType) -> Type -> SpecType
forall a b. (a -> b) -> a -> b
$ Var -> Type
tyVarKind Var
a)
  | Bool
otherwise
  = CGEnv -> CG CGEnv
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return CGEnv
γ

getExprFun :: CGEnv -> CoreExpr -> Var
getExprFun :: CGEnv -> Expr Var -> Var
getExprFun CGEnv
γ Expr Var
e          = Expr Var -> Var
forall {b}. Expr b -> Var
go Expr Var
e
  where
    go :: Expr b -> Var
go (App Expr b
x (Type Type
_)) = Expr b -> Var
go Expr b
x
    go (Var Var
x)          = Var
x
    go Expr b
_                = Maybe SrcSpan -> [Char] -> Var
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic (SrcSpan -> Maybe SrcSpan
forall a. a -> Maybe a
Just (CGEnv -> SrcSpan
getLocation CGEnv
γ)) [Char]
msg
    msg :: [Char]
msg                 = [Char]
"getFunName on \t" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Expr Var -> [Char]
forall a. Outputable a => a -> [Char]
GM.showPpr Expr Var
e

-- | `exprDict e` returns the dictionary `Var` inside the expression `e`
getExprDict :: CGEnv -> CoreExpr -> Maybe Var
getExprDict :: CGEnv -> Expr Var -> Maybe Var
getExprDict CGEnv
γ           =  Expr Var -> Maybe Var
forall {b}. Expr b -> Maybe Var
go
  where
    go :: Expr b -> Maybe Var
go (Var Var
x)          = case DEnv Var SpecType -> Var -> Maybe (HashMap Symbol (RISig SpecType))
forall k t.
(Eq k, Hashable k) =>
DEnv k t -> k -> Maybe (HashMap Symbol (RISig t))
dlookup (CGEnv -> DEnv Var SpecType
denv CGEnv
γ) Var
x of {Just HashMap Symbol (RISig SpecType)
_ -> Var -> Maybe Var
forall a. a -> Maybe a
Just Var
x; Maybe (HashMap Symbol (RISig SpecType))
Nothing -> Maybe Var
forall a. Maybe a
Nothing}
    go (Tick CoreTickish
_ Expr b
e)       = Expr b -> Maybe Var
go Expr b
e
    go (App Expr b
a (Type Type
_)) = Expr b -> Maybe Var
go Expr b
a
    go (Let Bind b
_ Expr b
e)        = Expr b -> Maybe Var
go Expr b
e
    go Expr b
_                = Maybe Var
forall a. Maybe a
Nothing

--------------------------------------------------------------------------------
-- | With GADTs and reflection, refinements can contain type variables,
--   as 'coercions' (see ucsd-progsys/#1424). At application sites, we
--   must also substitute those from the refinements (not just the types).
--      https://github.com/ucsd-progsys/liquidhaskell/issues/1424
--
--   see: tests/ple/{pos,neg}/T1424.hs
--
--------------------------------------------------------------------------------

subsTyReft :: CGEnv -> RTyVar -> Type -> SpecType -> SpecType
subsTyReft :: CGEnv -> RTyVar -> Type -> SpecType -> SpecType
subsTyReft CGEnv
γ RTyVar
a Type
t = (Symbol -> ExprBV Symbol Symbol -> ExprBV Symbol Symbol)
-> SpecType -> SpecType
forall b v c tv.
(b -> ExprBV b v -> ExprBV b v)
-> RTypeBV b v c tv (RReftBV b v) -> RTypeBV b v c tv (RReftBV b v)
mapExprReft (\Symbol
_ -> HashMap Symbol Sort -> ExprBV Symbol Symbol -> ExprBV Symbol Symbol
F.applyCoSub HashMap Symbol Sort
coSub)
  where
    coSub :: HashMap Symbol Sort
coSub        = [(Symbol, Sort)] -> HashMap Symbol Sort
forall k v. Hashable k => [(k, v)] -> HashMap k v
M.fromList [(RTyVar -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol RTyVar
a, TCEmb TyCon -> Type -> Sort
typeSort (CGEnv -> TCEmb TyCon
emb CGEnv
γ) Type
t)]

--------------------------------------------------------------------------------
-- | Type Synthesis for Special @Pattern@s -------------------------------------
--------------------------------------------------------------------------------
consPattern :: CGEnv -> Rs.Pattern -> Type -> CG SpecType

{- [NOTE] special type rule for monadic-bind application

    G |- e1 ~> m tx     G, x:tx |- e2 ~> m t
    -----------------------------------------
          G |- (e1 >>= \x -> e2) ~> m t
 -}

consPattern :: CGEnv -> Pattern -> Type -> StateT CGInfo Identity SpecType
consPattern CGEnv
γ (Rs.PatBind Expr Var
e1 Var
x Expr Var
e2 Type
_ Expr Var
_ Type
_ Type
_ Var
_) Type
_ = do
  tx <- ([Char], Expr Var) -> CGEnv -> SpecType -> SpecType
forall a.
Outputable a =>
([Char], a) -> CGEnv -> SpecType -> SpecType
checkMonad ([Char]
forall {a}. IsString a => a
msg, Expr Var
e1) CGEnv
γ (SpecType -> SpecType)
-> StateT CGInfo Identity SpecType
-> StateT CGInfo Identity SpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CGEnv -> Expr Var -> StateT CGInfo Identity SpecType
consE CGEnv
γ Expr Var
e1
  γ' <- γ += ("consPattern", F.symbol x, tx)
  addIdA x (AnnDef tx)
  consE γ' e2
  where
    msg :: a
msg = a
"This expression has a refined monadic type; run with --no-pattern-inline: "

{- [NOTE] special type rule for monadic-return

           G |- e ~> et
    ------------------------
      G |- return e ~ m et
 -}
consPattern CGEnv
γ (Rs.PatReturn Expr Var
e Type
m Expr Var
_ Type
_ Var
_) Type
t = do
  et    <- [Char] -> SpecType -> SpecType
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"Cons-Pattern-Ret" (SpecType -> SpecType)
-> StateT CGInfo Identity SpecType
-> StateT CGInfo Identity SpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CGEnv -> Expr Var -> StateT CGInfo Identity SpecType
consE CGEnv
γ Expr Var
e
  mt    <- trueTy (typeclass (getConfig γ))  m
  tt    <- trueTy (typeclass (getConfig γ))  t
  return (mkRAppTy mt et tt) -- /// {-    $ RAppTy mt et mempty -}

{- [NOTE] special type rule for field projection, is
          t  = G(x)       ti = Proj(t, i)
    -----------------------------------------
      G |- case x of C [y1...yn] -> yi : ti
 -}

consPattern CGEnv
γ (Rs.PatProject Var
xe Var
_ Type
τ DataCon
c [Var]
ys Int
i) Type
_ = do
  let yi :: Var
yi = [Var]
ys [Var] -> Int -> Var
forall a. HasCallStack => [a] -> Int -> a
!! Int
i
  t    <- Bool
-> KVKind -> Expr Var -> Type -> StateT CGInfo Identity SpecType
freshTyType (Config -> Bool
typeclass (CGEnv -> Config
forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)) KVKind
ProjectE (Var -> Expr Var
forall b. Var -> Expr b
Var Var
yi) Type
τ
  _    <- (addW . WfC γ) t
  γ'   <- caseEnv γ xe [] (DataAlt c) ys (Just [i])
  ti   <- {- γ' ??= yi -} varRefType γ' yi
  addC (SubC γ' ti t) "consPattern:project"
  return t

consPattern CGEnv
γ (Rs.PatSelfBind Var
_ Expr Var
e) Type
_ =
  CGEnv -> Expr Var -> StateT CGInfo Identity SpecType
consE CGEnv
γ Expr Var
e

consPattern CGEnv
γ p :: Pattern
p@Rs.PatSelfRecBind{} Type
_ =
  KVKind -> CGEnv -> Expr Var -> StateT CGInfo Identity SpecType
cconsFreshE KVKind
LetE CGEnv
γ (Pattern -> Expr Var
Rs.lower Pattern
p)

mkRAppTy :: SpecType -> SpecType -> SpecType -> SpecType
mkRAppTy :: SpecType -> SpecType -> SpecType -> SpecType
mkRAppTy SpecType
mt SpecType
et RAppTy{}          = SpecType -> SpecType -> RReft -> SpecType
forall b v c tv r.
RTypeBV b v c tv r -> RTypeBV b v c tv r -> r -> RTypeBV b v c tv r
RAppTy SpecType
mt SpecType
et RReft
forall a. Monoid a => a
mempty
mkRAppTy SpecType
_  SpecType
et (RApp RTyCon
c [SpecType
_] [] RReft
_) = RTyCon
-> [SpecType] -> [RTProp RTyCon RTyVar RReft] -> RReft -> 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
et] [] RReft
forall a. Monoid a => a
mempty
mkRAppTy SpecType
_  SpecType
_  SpecType
_                 = Maybe SrcSpan -> [Char] -> SpecType
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing [Char]
"Unexpected return-pattern"

checkMonad :: (Outputable a) => (String, a) -> CGEnv -> SpecType -> SpecType
checkMonad :: forall a.
Outputable a =>
([Char], a) -> CGEnv -> SpecType -> SpecType
checkMonad ([Char], a)
x CGEnv
g = SpecType -> SpecType
go (SpecType -> SpecType)
-> (SpecType -> SpecType) -> SpecType -> SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SpecType -> SpecType
unRRTy
 where
   go :: SpecType -> SpecType
go (RApp RTyCon
_ [SpecType]
ts [] RReft
_)
     | Bool -> Bool
not ([SpecType] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SpecType]
ts) = [SpecType] -> SpecType
forall a. HasCallStack => [a] -> a
last [SpecType]
ts
   go (RAppTy SpecType
_ SpecType
t RReft
_) = SpecType
t
   go SpecType
t              = ([Char], a) -> CGEnv -> SpecType -> SpecType
forall a.
Outputable a =>
([Char], a) -> CGEnv -> SpecType -> SpecType
checkErr ([Char], a)
x CGEnv
g SpecType
t

unRRTy :: SpecType -> SpecType
unRRTy :: SpecType -> SpecType
unRRTy (RRTy [(Symbol, SpecType)]
_ RReft
_ Oblig
_ SpecType
t) = SpecType -> SpecType
unRRTy SpecType
t
unRRTy SpecType
t              = SpecType
t

--------------------------------------------------------------------------------
castTy  :: CGEnv -> Type -> CoreExpr -> Coercion -> CG SpecType
castTy' :: CGEnv -> Type -> CoreExpr -> CG SpecType
--------------------------------------------------------------------------------
castTy :: CGEnv
-> Type -> Expr Var -> CoercionR -> StateT CGInfo Identity SpecType
castTy CGEnv
γ Type
t Expr Var
e (AxiomCo CoAxiomRule
ca [CoercionR]
_)
  = do
    msp <- case CoAxiomRule -> Maybe (TyCon, CoAxBranch)
isNewtypeAxiomRule_maybe CoAxiomRule
ca of
      Just (TyCon
tc, CoAxBranch
_) -> TyCon -> StateT CGInfo Identity (Maybe SpecType)
lookupNewType TyCon
tc
      Maybe (TyCon, CoAxBranch)
_ -> Maybe SpecType -> StateT CGInfo Identity (Maybe SpecType)
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe SpecType
forall a. Maybe a
Nothing
    sp <- castTy' γ t e
    return (fromMaybe sp msp)

castTy CGEnv
γ Type
t Expr Var
e (SymCo (AxiomCo CoAxiomRule
ca [CoercionR]
_))
  = do mtc <- case CoAxiomRule -> Maybe (TyCon, CoAxBranch)
isNewtypeAxiomRule_maybe CoAxiomRule
ca of
         Just (TyCon
tc, CoAxBranch
_) -> TyCon -> StateT CGInfo Identity (Maybe SpecType)
lookupNewType TyCon
tc
         Maybe (TyCon, CoAxBranch)
_ -> Maybe SpecType -> StateT CGInfo Identity (Maybe SpecType)
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe SpecType
forall a. Maybe a
Nothing
       F.forM_ mtc (cconsE γ e)
       castTy' γ t e

castTy CGEnv
γ Type
t Expr Var
e CoercionR
_
  = CGEnv -> Type -> Expr Var -> StateT CGInfo Identity SpecType
castTy' CGEnv
γ Type
t Expr Var
e


castTy' :: CGEnv -> Type -> Expr Var -> StateT CGInfo Identity SpecType
castTy' CGEnv
γ Type
τ (Var Var
x)
  = do t0 <- Bool -> Type -> StateT CGInfo Identity SpecType
trueTy (Config -> Bool
typeclass (CGEnv -> Config
forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)) Type
τ
       tx <- varRefType γ x
       let t = SpecType -> SpecType -> SpecType
mergeCastTys SpecType
t0 SpecType
tx
       let ce = if Config -> Bool
typeclass (CGEnv -> Config
forall t. HasConfig t => t -> Config
getConfig CGEnv
γ) then Var -> ExprBV Symbol Symbol
forall a. Expression a => a -> ExprBV Symbol Symbol
F.expr Var
x
                  else Sort -> Sort -> ExprBV Symbol Symbol -> ExprBV Symbol Symbol
forall {b} {v}. Sort -> Sort -> ExprBV b v -> ExprBV b v
eCoerc (TCEmb TyCon -> Type -> Sort
typeSort (CGEnv -> TCEmb TyCon
emb CGEnv
γ) (Type -> Sort) -> Type -> Sort
forall a b. (a -> b) -> a -> b
$ Type -> Type
Ghc.expandTypeSynonyms (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Var -> Type
varType Var
x)
                         (TCEmb TyCon -> Type -> Sort
typeSort (CGEnv -> TCEmb TyCon
emb CGEnv
γ) Type
τ)
                         (ExprBV Symbol Symbol -> ExprBV Symbol Symbol)
-> ExprBV Symbol Symbol -> ExprBV Symbol Symbol
forall a b. (a -> b) -> a -> b
$ Var -> ExprBV Symbol Symbol
forall a. Expression a => a -> ExprBV Symbol Symbol
F.expr Var
x
       return (t `strengthen` uTop (F.uexprReft ce) {- `meet` tx -})
  where eCoerc :: Sort -> Sort -> ExprBV b v -> ExprBV b v
eCoerc Sort
s Sort
t ExprBV b v
e
         | Sort
s Sort -> Sort -> Bool
forall a. Eq a => a -> a -> Bool
== Sort
t    = ExprBV b v
e
         | Bool
otherwise = Sort -> Sort -> ExprBV b v -> ExprBV b v
forall {b} {v}. Sort -> Sort -> ExprBV b v -> ExprBV b v
F.ECoerc Sort
s Sort
t ExprBV b v
e

castTy' CGEnv
γ Type
t (Tick CoreTickish
_ Expr Var
e)
  = CGEnv -> Type -> Expr Var -> StateT CGInfo Identity SpecType
castTy' CGEnv
γ Type
t Expr Var
e

castTy' CGEnv
_ Type
_ Expr Var
e
  = Maybe SrcSpan -> [Char] -> StateT CGInfo Identity SpecType
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing ([Char] -> StateT CGInfo Identity SpecType)
-> [Char] -> StateT CGInfo Identity SpecType
forall a b. (a -> b) -> a -> b
$ [Char]
"castTy cannot handle expr " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Expr Var -> [Char]
forall a. Outputable a => a -> [Char]
GM.showPpr Expr Var
e


{-
mergeCastTys tcorrect trefined
  tcorrect has the correct GHC skeleton,
  trefined has the correct refinements (before coercion)
  mergeCastTys keeps the trefined when the two GHC types match
-}

mergeCastTys :: SpecType -> SpecType -> SpecType
mergeCastTys :: SpecType -> SpecType -> SpecType
mergeCastTys SpecType
t1 SpecType
t2
  | Bool -> SpecType -> Type
forall r. ToTypeable r => Bool -> RRType r -> Type
toType Bool
False SpecType
t1 Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Bool -> SpecType -> Type
forall r. ToTypeable r => Bool -> RRType r -> Type
toType Bool
False SpecType
t2
  = SpecType
t2
mergeCastTys (RApp RTyCon
c1 [SpecType]
ts1 [RTProp RTyCon RTyVar RReft]
ps1 RReft
r1) (RApp RTyCon
c2 [SpecType]
ts2 [RTProp RTyCon RTyVar RReft]
_ RReft
_)
  | RTyCon
c1 RTyCon -> RTyCon -> Bool
forall a. Eq a => a -> a -> Bool
== RTyCon
c2
  = RTyCon
-> [SpecType] -> [RTProp RTyCon RTyVar RReft] -> RReft -> 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
c1 ((SpecType -> SpecType -> SpecType)
-> [SpecType] -> [SpecType] -> [SpecType]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith SpecType -> SpecType -> SpecType
mergeCastTys [SpecType]
ts1 [SpecType]
ts2) [RTProp RTyCon RTyVar RReft]
ps1 RReft
r1
mergeCastTys SpecType
t SpecType
_
  = SpecType
t

{-
showCoercion :: Coercion -> String
showCoercion (AxiomInstCo co1 co2 co3)
  = "AxiomInstCo " ++ showPpr co1 ++ "\t\t " ++ showPpr co2 ++ "\t\t" ++ showPpr co3 ++ "\n\n" ++
    "COAxiom Tycon = "  ++ showPpr (coAxiomTyCon co1) ++ "\nBRANCHES\n" ++ concatMap showBranch bs
  where
    bs = fromBranchList $ co_ax_branches co1
    showBranch ab = "\nCoAxiom \nLHS = " ++ showPpr (coAxBranchLHS ab) ++
                    "\nRHS = " ++ showPpr (coAxBranchRHS ab)
showCoercion (SymCo c)
  = "Symc :: " ++ showCoercion c
showCoercion c
  = "Coercion " ++ showPpr c
-}

isClassConCo :: Coercion -> Maybe (Expr Var -> Expr Var)
-- See Note [Type classes with a single method]
isClassConCo :: CoercionR -> Maybe (Expr Var -> Expr Var)
isClassConCo CoercionR
co
  | Pair Type
t1 Type
t2 <- HasDebugCallStack => CoercionR -> Pair Type
CoercionR -> Pair Type
coercionKind CoercionR
co
  , Type -> Bool
isClassPred Type
t2
  , (TyCon
tc,[Type]
ts) <- Type -> (TyCon, [Type])
splitTyConApp Type
t2
  , [DataCon
dc]    <- TyCon -> [DataCon]
tyConDataCons TyCon
tc
  , [Type
tm]    <- (Scaled Type -> Type) -> [Scaled Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Scaled Type -> Type
forall a. Scaled a -> a
irrelevantMult (DataCon -> [Scaled Type]
Ghc.dataConOrigArgTys DataCon
dc)
               -- tcMatchTy because we have to instantiate the class tyvars
  , Just TvSubstEnv
_  <- TyCoVarSet
-> RnEnv2 -> TvSubstEnv -> Type -> Type -> Maybe TvSubstEnv
ruleMatchTyX ([Var] -> TyCoVarSet
forall a. Uniquable a => [a] -> UniqSet a
mkUniqSet ([Var] -> TyCoVarSet) -> [Var] -> TyCoVarSet
forall a b. (a -> b) -> a -> b
$ TyCon -> [Var]
tyConTyVars TyCon
tc) (InScopeSet -> RnEnv2
mkRnEnv2 InScopeSet
emptyInScopeSet) TvSubstEnv
emptyTvSubstEnv Type
tm Type
t1
  = (Expr Var -> Expr Var) -> Maybe (Expr Var -> Expr Var)
forall a. a -> Maybe a
Just (\Expr Var
e -> DataCon -> [Expr Var] -> Expr Var
mkCoreConApps DataCon
dc ([Expr Var] -> Expr Var) -> [Expr Var] -> Expr Var
forall a b. (a -> b) -> a -> b
$ (Type -> Expr Var) -> [Type] -> [Expr Var]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Expr Var
forall b. Type -> Expr b
Type [Type]
ts [Expr Var] -> [Expr Var] -> [Expr Var]
forall a. [a] -> [a] -> [a]
++ [Expr Var
e])

  | Bool
otherwise
  = Maybe (Expr Var -> Expr Var)
forall a. Maybe a
Nothing
  where
    ruleMatchTyX :: TyCoVarSet
-> RnEnv2 -> TvSubstEnv -> Type -> Type -> Maybe TvSubstEnv
ruleMatchTyX = TyCoVarSet
-> RnEnv2 -> TvSubstEnv -> Type -> Type -> Maybe TvSubstEnv
ruleMatchTyKiX -- TODO: is this correct?

----------------------------------------------------------------------
-- Note [Type classes with a single method]
----------------------------------------------------------------------
-- GHC 7.10 encodes type classes with a single method as newtypes and
-- `cast`s between the method and class type instead of applying the
-- class constructor. Just rewrite the core to what we're used to
-- seeing..
--
-- specifically, we want to rewrite
--
--   e `cast` ((a -> b) ~ C)
--
-- to
--
--   D:C e
--
-- but only when
--
--   D:C :: (a -> b) -> C

--------------------------------------------------------------------------------
-- | @consFreshE@ is used to *synthesize* types with a **fresh template**.
--   e.g. at joins, recursive binders, polymorphic instantiations etc. It is
--   the "portal" that connects `consE` (synthesis) and `cconsE` (checking)
--------------------------------------------------------------------------------
cconsFreshE :: KVKind -> CGEnv -> CoreExpr -> CG SpecType
cconsFreshE :: KVKind -> CGEnv -> Expr Var -> StateT CGInfo Identity SpecType
cconsFreshE KVKind
kvkind CGEnv
γ Expr Var
e = do
  t   <- Bool
-> KVKind -> Expr Var -> Type -> StateT CGInfo Identity SpecType
freshTyType (Config -> Bool
typeclass (CGEnv -> Config
forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)) KVKind
kvkind Expr Var
e (Type -> StateT CGInfo Identity SpecType)
-> Type -> StateT CGInfo Identity SpecType
forall a b. (a -> b) -> a -> b
$ HasDebugCallStack => Expr Var -> Type
Expr Var -> Type
exprType Expr Var
e
  addW $ WfC γ t
  cconsE γ e t
  return t
--------------------------------------------------------------------------------

checkUnbound :: (Show a, Show a2, F.Subable a, F.Variable a ~ F.Symbol)
             => CGEnv -> CoreExpr -> F.Symbol -> a -> a2 -> a
checkUnbound :: forall a a2.
(Show a, Show a2, Subable a, Variable a ~ Symbol) =>
CGEnv -> Expr Var -> Symbol -> a -> a2 -> a
checkUnbound CGEnv
γ Expr Var
e Symbol
x a
t a2
a
  | Symbol
x Symbol -> [Symbol] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` a -> [Variable a]
forall a. Subable a => a -> [Variable a]
F.syms a
t = a
t
  | Bool
otherwise            = Maybe SrcSpan -> [Char] -> a
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic (SrcSpan -> Maybe SrcSpan
forall a. a -> Maybe a
Just (SrcSpan -> Maybe SrcSpan) -> SrcSpan -> Maybe SrcSpan
forall a b. (a -> b) -> a -> b
$ CGEnv -> SrcSpan
getLocation CGEnv
γ) [Char]
msg
  where
    msg :: [Char]
msg = [[Char]] -> [Char]
unlines [ [Char]
"checkUnbound: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Symbol -> [Char]
forall a. Show a => a -> [Char]
show Symbol
x [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" is elem of syms of " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. Show a => a -> [Char]
show a
t
                  , [Char]
"In"
                  , Expr Var -> [Char]
forall a. Outputable a => a -> [Char]
GM.showPpr Expr Var
e
                  , [Char]
"Arg = "
                  , a2 -> [Char]
forall a. Show a => a -> [Char]
show a2
a
                  ]

dropExists :: CGEnv -> SpecType -> CG (CGEnv, SpecType)
dropExists :: CGEnv -> SpecType -> CG (CGEnv, SpecType)
dropExists CGEnv
γ (REx Symbol
x SpecType
tx SpecType
t) =         (, SpecType
t) (CGEnv -> (CGEnv, SpecType)) -> CG CGEnv -> CG (CGEnv, SpecType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CGEnv
γ CGEnv -> ([Char], Symbol, SpecType) -> CG CGEnv
+= ([Char]
"dropExists", Symbol
x, SpecType
tx)
dropExists CGEnv
γ SpecType
t            = (CGEnv, SpecType) -> CG (CGEnv, SpecType)
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (CGEnv
γ, SpecType
t)

dropConstraints :: CGEnv -> SpecType -> CG SpecType
dropConstraints :: CGEnv -> SpecType -> StateT CGInfo Identity SpecType
dropConstraints CGEnv
cgenv (RFun Symbol
x RFInfo
i tx :: SpecType
tx@(RApp RTyCon
c [SpecType]
_ [RTProp RTyCon RTyVar RReft]
_ RReft
_) SpecType
t RReft
r) | RTyCon -> Bool
forall {c}. TyConable c => c -> Bool
isErasable RTyCon
c
  = (SpecType -> RReft -> SpecType) -> RReft -> SpecType -> SpecType
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Symbol -> RFInfo -> SpecType -> SpecType -> RReft -> SpecType
forall b v c tv r.
b
-> RFInfo
-> RTypeBV b v c tv r
-> RTypeBV b v c tv r
-> r
-> RTypeBV b v c tv r
RFun Symbol
x RFInfo
i SpecType
tx) RReft
r (SpecType -> SpecType)
-> StateT CGInfo Identity SpecType
-> StateT CGInfo Identity SpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CGEnv -> SpecType -> StateT CGInfo Identity SpecType
dropConstraints CGEnv
cgenv SpecType
t
  where
    isErasable :: c -> Bool
isErasable = if Config -> Bool
typeclass (CGEnv -> Config
forall t. HasConfig t => t -> Config
getConfig CGEnv
cgenv) then c -> Bool
forall {c}. TyConable c => c -> Bool
isEmbeddedDict else c -> Bool
forall {c}. TyConable c => c -> Bool
isClass
dropConstraints CGEnv
cgenv (RRTy [(Symbol, SpecType)]
cts RReft
_ Oblig
OCons SpecType
rt)
  = do γ' <- (CGEnv -> (Symbol, SpecType) -> CG CGEnv)
-> CGEnv -> [(Symbol, SpecType)] -> CG CGEnv
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\CGEnv
γ (Symbol
x, SpecType
t) -> CGEnv
γ CGEnv -> ([Char], Symbol, SpecType) -> CG CGEnv
`addSEnv` ([Char]
"splitS", Symbol
x,SpecType
t)) CGEnv
cgenv [(Symbol, SpecType)]
xts
       addC (SubC γ' t1 t2)  "dropConstraints"
       dropConstraints cgenv rt
  where
    ([(Symbol, SpecType)]
xts, SpecType
t1, SpecType
t2) = [(Symbol, SpecType)] -> ([(Symbol, SpecType)], SpecType, SpecType)
forall a b. [(a, b)] -> ([(a, b)], b, b)
envToSub [(Symbol, SpecType)]
cts

dropConstraints CGEnv
_ SpecType
t = SpecType -> StateT CGInfo Identity SpecType
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return SpecType
t

-------------------------------------------------------------------------------------
cconsCase :: CGEnv -> Var -> SpecType -> [AltCon] -> CoreAlt -> CG ()
-------------------------------------------------------------------------------------
cconsCase :: CGEnv -> Var -> SpecType -> [AltCon] -> Alt Var -> State CGInfo ()
cconsCase CGEnv
γ Var
x SpecType
t [AltCon]
acs (Alt AltCon
ac [Var]
ys Expr Var
ce)
  = do cγ <- CGEnv
-> Var -> [AltCon] -> AltCon -> [Var] -> Maybe [Int] -> CG CGEnv
caseEnv CGEnv
γ Var
x [AltCon]
acs AltCon
ac [Var]
ys Maybe [Int]
forall a. Monoid a => a
mempty
       cconsE cγ ce t

{-

case x :: List b of
  Emp -> e

  Emp :: tdc          forall a. {v: List a | cons v === 0}
  x   :: xt           List b
  ys  == binders      []

-}
-------------------------------------------------------------------------------------
caseEnv   :: CGEnv -> Var -> [AltCon] -> AltCon -> [Var] -> Maybe [Int] -> CG CGEnv
-------------------------------------------------------------------------------------
caseEnv :: CGEnv
-> Var -> [AltCon] -> AltCon -> [Var] -> Maybe [Int] -> CG CGEnv
caseEnv CGEnv
γ Var
x [AltCon]
_   (DataAlt DataCon
c) [Var]
ys Maybe [Int]
pIs = do

  let (Symbol
x' : [Symbol]
ys')   = Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (Var -> Symbol) -> [Var] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Var
xVar -> [Var] -> [Var]
forall a. a -> [a] -> [a]
:[Var]
ys)
  xt0             <- ([Char], Var) -> CGEnv -> SpecType -> SpecType
forall a.
Outputable a =>
([Char], a) -> CGEnv -> SpecType -> SpecType
checkTyCon ([Char]
"checkTycon cconsCase", Var
x) CGEnv
γ (SpecType -> SpecType)
-> StateT CGInfo Identity SpecType
-> StateT CGInfo Identity SpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CGEnv
γ HasCallStack => CGEnv -> Var -> StateT CGInfo Identity SpecType
CGEnv -> Var -> StateT CGInfo Identity SpecType
??= Var
x
  let rt           = 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
xt0 Symbol
x'
  tdc             <- γ ??= dataConWorkId c >>= refreshVV
  let (rtd,yts',_) = unfoldR tdc rt ys
  yts             <- projectTypes (typeclass (getConfig γ))  pIs yts'
  let ys''         = Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (Var -> Symbol) -> [Var] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Var -> Bool) -> [Var] -> [Var]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Var -> Bool) -> Var -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. if Bool
allowTC then Var -> Bool
GM.isEmbeddedDictVar else Var -> Bool
GM.isEvVar) [Var]
ys
  let r1           = DataCon -> [Symbol] -> ReftBV Symbol Symbol
dataConReft   DataCon
c   [Symbol]
ys''
  let r2           = SpecType -> [Symbol] -> ReftBV Symbol Symbol
forall r v c tv.
(ToReft r, ReftBind r ~ v, ReftVar r ~ v, Refreshable v) =>
RTypeBV v v c tv r -> [v] -> ReftBV v v
dataConMsReft SpecType
rtd [Symbol]
ys''
  let xt           = (SpecType
xt0 SpecType -> SpecType -> SpecType
forall r. Meet r => r -> r -> r
`meet` SpecType
rtd) SpecType -> RReft -> SpecType
forall r b v c tv.
Meet r =>
RTypeBV b v c tv r -> r -> RTypeBV b v c tv r
`strengthen` ReftBV Symbol Symbol -> RReft
forall r v. r -> UReftV v r
uTop (ReftBV Symbol Symbol
r1 ReftBV Symbol Symbol
-> ReftBV Symbol Symbol -> ReftBV Symbol Symbol
forall r. Meet r => r -> r -> r
`meet` ReftBV Symbol Symbol
r2)
  let cbs          = [Char] -> [Symbol] -> [SpecType] -> [(Symbol, SpecType)]
forall a b. HasCallStack => [Char] -> [a] -> [b] -> [(a, b)]
safeZip [Char]
"cconsCase" (Symbol
x'Symbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
:[Symbol]
ys')
                         ((SpecType -> SpecType) -> [SpecType] -> [SpecType]
forall a b. (a -> b) -> [a] -> [b]
map (SpecType
-> (Variable SpecType,
    ExprBV (Variable SpecType) (Variable SpecType))
-> SpecType
forall a.
Subable a =>
a -> (Variable a, ExprBV (Variable a) (Variable a)) -> a
`F.subst1` (Symbol
Variable SpecType
selfSymbol, Symbol -> ExprBV Symbol Symbol
forall b v. v -> ExprBV b v
F.EVar Symbol
x'))
                         (SpecType
xt0 SpecType -> [SpecType] -> [SpecType]
forall a. a -> [a] -> [a]
: [SpecType]
yts))
  cγ'  <- addBinders γ   x' cbs
  when allowDC $
    addRewritesForNextBinding $ getCaseRewrites γ $ xt0 `meet` rtd
  addBinders cγ' x' [(x', substSelf <$> xt)]
  where allowTC :: Bool
allowTC    = Config -> Bool
typeclass (CGEnv -> Config
forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)
        allowDC :: Bool
allowDC    = Config -> Bool
dependantCase (CGEnv -> Config
forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)

caseEnv CGEnv
γ Var
x [AltCon]
acs AltCon
a [Var]
_ Maybe [Int]
_ = do
  let x' :: Symbol
x'  = Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
x
  xt'    <- (SpecType -> RReft -> SpecType
forall r b v c tv.
Meet r =>
RTypeBV b v c tv r -> r -> RTypeBV b v c tv r
`strengthen` ReftBV Symbol Symbol -> RReft
forall r v. r -> UReftV v r
uTop (CGEnv -> [AltCon] -> AltCon -> ReftBV Symbol Symbol
altReft CGEnv
γ [AltCon]
acs AltCon
a)) (SpecType -> SpecType)
-> StateT CGInfo Identity SpecType
-> StateT CGInfo Identity SpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (CGEnv
γ HasCallStack => CGEnv -> Var -> StateT CGInfo Identity SpecType
CGEnv -> Var -> StateT CGInfo Identity SpecType
??= Var
x)
  addBinders γ x' [(x', xt')]


------------------------------------------------------
-- SELF special substitutions
------------------------------------------------------

substSelf :: UReft F.Reft -> UReft F.Reft
substSelf :: RReft -> RReft
substSelf (MkUReft ReftBV Symbol Symbol
r PredicateBV Symbol Symbol
p) = ReftBV Symbol Symbol -> PredicateBV Symbol Symbol -> RReft
forall b v r. r -> PredicateBV b v -> UReftBV b v r
MkUReft (ReftBV Symbol Symbol -> ReftBV Symbol Symbol
substSelfReft ReftBV Symbol Symbol
r) PredicateBV Symbol Symbol
p

substSelfReft :: F.Reft -> F.Reft
substSelfReft :: ReftBV Symbol Symbol -> ReftBV Symbol Symbol
substSelfReft (F.Reft (Symbol
v, ExprBV Symbol Symbol
e)) = (Symbol, ExprBV Symbol Symbol) -> ReftBV Symbol Symbol
forall b v. (b, ExprBV b v) -> ReftBV b v
F.Reft (Symbol
v, ExprBV Symbol Symbol
-> (Variable (ExprBV Symbol Symbol),
    ExprBV
      (Variable (ExprBV Symbol Symbol))
      (Variable (ExprBV Symbol Symbol)))
-> ExprBV Symbol Symbol
forall a.
Subable a =>
a -> (Variable a, ExprBV (Variable a) (Variable a)) -> a
F.subst1 ExprBV Symbol Symbol
e (Symbol
Variable (ExprBV Symbol Symbol)
selfSymbol, Symbol -> ExprBV Symbol Symbol
forall b v. v -> ExprBV b v
F.EVar Symbol
v))

ignoreSelf :: F.Reft -> F.Reft
ignoreSelf :: ReftBV Symbol Symbol -> ReftBV Symbol Symbol
ignoreSelf = (ExprBV Symbol Symbol -> ExprBV Symbol Symbol)
-> ReftBV Symbol Symbol -> ReftBV Symbol Symbol
forall t.
Visitable t =>
(ExprBV Symbol Symbol -> ExprBV Symbol Symbol) -> t -> t
F.mapExpr (\ExprBV Symbol Symbol
r -> if Symbol
selfSymbol Symbol -> [Symbol] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ExprBV Symbol Symbol -> [Variable (ExprBV Symbol Symbol)]
forall a. Subable a => a -> [Variable a]
F.syms ExprBV Symbol Symbol
r then ExprBV Symbol Symbol
forall b v. ExprBV b v
F.PTrue else ExprBV Symbol Symbol
r)

--------------------------------------------------------------------------------
-- | `projectTypes` masks (i.e. true's out) all types EXCEPT those
--   at given indices; it is used to simplify the environment used
--   when projecting out fields of single-ctor datatypes.
--------------------------------------------------------------------------------
projectTypes :: Bool -> Maybe [Int] -> [SpecType] -> CG [SpecType]
projectTypes :: Bool
-> Maybe [Int] -> [SpecType] -> StateT CGInfo Identity [SpecType]
projectTypes Bool
_        Maybe [Int]
Nothing    [SpecType]
ts = [SpecType] -> StateT CGInfo Identity [SpecType]
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return [SpecType]
ts
projectTypes Bool
allowTC (Just [Int]
ints) [SpecType]
ts = ((Int, SpecType) -> StateT CGInfo Identity SpecType)
-> [(Int, SpecType)] -> StateT CGInfo Identity [SpecType]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ([Int] -> (Int, SpecType) -> StateT CGInfo Identity SpecType
forall {t :: * -> *} {a} {m :: * -> *} {a}.
(Foldable t, Eq a, Freshable m a) =>
t a -> (a, a) -> m a
projT [Int]
ints) ([Int] -> [SpecType] -> [(Int, SpecType)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] [SpecType]
ts)
  where
    projT :: t a -> (a, a) -> m a
projT t a
is (a
j, a
t)
      | a
j a -> t a -> Bool
forall a. Eq a => a -> t a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t a
is = a -> m a
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
t
      | Bool
otherwise   = Bool -> a -> m a
forall (m :: * -> *) a. Freshable m a => Bool -> a -> m a
true Bool
allowTC a
t

altReft :: CGEnv -> [AltCon] -> AltCon -> F.Reft
altReft :: CGEnv -> [AltCon] -> AltCon -> ReftBV Symbol Symbol
altReft CGEnv
_ [AltCon]
_   (LitAlt Literal
l) = Literal -> ReftBV Symbol Symbol
literalFReft Literal
l
altReft CGEnv
γ [AltCon]
acs AltCon
DEFAULT    = [ReftBV Symbol Symbol] -> ReftBV Symbol Symbol
forall a. Monoid a => [a] -> a
mconcat ([Literal -> ReftBV Symbol Symbol
notLiteralReft Literal
l | LitAlt Literal
l <- [AltCon]
acs] [ReftBV Symbol Symbol]
-> [ReftBV Symbol Symbol] -> [ReftBV Symbol Symbol]
forall a. [a] -> [a] -> [a]
++ [DataCon -> ReftBV Symbol Symbol
notDataConReft DataCon
d | DataAlt DataCon
d <- [AltCon]
acs])
  where
    notLiteralReft :: Literal -> ReftBV Symbol Symbol
notLiteralReft   = ReftBV Symbol Symbol
-> (ExprBV Symbol Symbol -> ReftBV Symbol Symbol)
-> Maybe (ExprBV Symbol Symbol)
-> ReftBV Symbol Symbol
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ReftBV Symbol Symbol
forall a. Monoid a => a
mempty ExprBV Symbol Symbol -> ReftBV Symbol Symbol
forall a. Expression a => a -> ReftBV Symbol Symbol
F.notExprReft (Maybe (ExprBV Symbol Symbol) -> ReftBV Symbol Symbol)
-> (Literal -> Maybe (ExprBV Symbol Symbol))
-> Literal
-> ReftBV Symbol Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Sort, Maybe (ExprBV Symbol Symbol))
-> Maybe (ExprBV Symbol Symbol)
forall a b. (a, b) -> b
snd ((Sort, Maybe (ExprBV Symbol Symbol))
 -> Maybe (ExprBV Symbol Symbol))
-> (Literal -> (Sort, Maybe (ExprBV Symbol Symbol)))
-> Literal
-> Maybe (ExprBV Symbol Symbol)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCEmb TyCon -> Literal -> (Sort, Maybe (ExprBV Symbol Symbol))
literalConst (CGEnv -> TCEmb TyCon
emb CGEnv
γ)
    notDataConReft :: DataCon -> ReftBV Symbol Symbol
notDataConReft DataCon
d = (Symbol, ExprBV Symbol Symbol) -> ReftBV Symbol Symbol
forall b v. (b, ExprBV b v) -> ReftBV b v
F.Reft (Symbol
F.vv_, ExprBV Symbol Symbol -> ExprBV Symbol Symbol
forall {b} {v}. ExprBV b v -> ExprBV b v
F.PNot (ExprBV Symbol Symbol
-> ExprBV Symbol Symbol -> ExprBV Symbol Symbol
forall b v. ExprBV b v -> ExprBV b v -> ExprBV b v
F.EApp (Symbol -> ExprBV Symbol Symbol
forall b v. v -> ExprBV b v
F.EVar (Symbol -> ExprBV Symbol Symbol) -> Symbol -> ExprBV Symbol Symbol
forall a b. (a -> b) -> a -> b
$ DataCon -> Symbol
makeDataConChecker DataCon
d) (Symbol -> ExprBV Symbol Symbol
forall b v. v -> ExprBV b v
F.EVar Symbol
F.vv_)))
altReft CGEnv
_ [AltCon]
_ AltCon
_            = Maybe SrcSpan -> [Char] -> ReftBV Symbol Symbol
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing [Char]
"Constraint : altReft"

unfoldR :: SpecType -> SpecType -> [Var] -> (SpecType, [SpecType], SpecType)
unfoldR :: SpecType -> SpecType -> [Var] -> (SpecType, [SpecType], SpecType)
unfoldR SpecType
td (RApp RTyCon
_ [SpecType]
ts [RTProp RTyCon RTyVar RReft]
rs RReft
_) [Var]
ys = (SpecType
t3, [SpecType]
forall {r}. IsReft r => [RTypeBV Symbol Symbol RTyCon RTyVar r]
tvys [SpecType] -> [SpecType] -> [SpecType]
forall a. [a] -> [a] -> [a]
++ [SpecType]
yts, SpecType -> SpecType
forall b v c tv r. RTypeBV b v c tv r -> RTypeBV b v c tv r
ignoreOblig SpecType
rt)
  where
        tbody :: SpecType
tbody                = SpecType -> [RTProp RTyCon RTyVar RReft] -> SpecType
instantiatePvs (SpecType -> [SpecType] -> SpecType
instantiateTys SpecType
td [SpecType]
ts) ([RTProp RTyCon RTyVar RReft] -> [RTProp RTyCon RTyVar RReft]
forall a. [a] -> [a]
reverse [RTProp RTyCon RTyVar RReft]
rs)
        (([Symbol]
ys0,[RFInfo]
_,[SpecType]
yts',[RReft]
_), SpecType
rt) = SpecType -> (([Symbol], [RFInfo], [SpecType], [RReft]), SpecType)
forall t t1 a.
PPrint (RType t t1 a) =>
RType t t1 a
-> (([Symbol], [RFInfo], [RType t t1 a], [a]), RType t t1 a)
safeBkArrow ([Char] -> SpecType -> SpecType
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
msg (SpecType -> SpecType) -> SpecType -> SpecType
forall a b. (a -> b) -> a -> b
$ SpecType -> [SpecType] -> SpecType
instantiateTys SpecType
tbody [SpecType]
tvs')
        msg :: [Char]
msg                  = [Char]
"INST-TY: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (SpecType, [SpecType], SpecType, [Var], [SpecType]) -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp (SpecType
td, [SpecType]
ts, SpecType
tbody, [Var]
ys, [SpecType]
tvs')
        yts'' :: [SpecType]
yts''                = (SubstV Symbol -> SpecType -> SpecType)
-> [SubstV Symbol] -> [SpecType] -> [SpecType]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith SubstV Symbol -> SpecType -> SpecType
SubstV (Variable SpecType) -> SpecType -> SpecType
forall a.
(Subable a, HasCallStack) =>
SubstV (Variable a) -> a -> a
F.subst [SubstV Symbol]
sus ([SpecType]
yts'[SpecType] -> [SpecType] -> [SpecType]
forall a. [a] -> [a] -> [a]
++[SpecType
rt])
        (SpecType
t3,[SpecType]
yts)             = ([SpecType] -> SpecType
forall a. HasCallStack => [a] -> a
last [SpecType]
yts'', [SpecType] -> [SpecType]
forall a. HasCallStack => [a] -> [a]
init [SpecType]
yts'')
        sus :: [SubstV Symbol]
sus                  = [(Symbol, ExprBV Symbol Symbol)] -> SubstV Symbol
forall v. Hashable v => [(v, ExprBV v v)] -> SubstV v
F.mkSubst ([(Symbol, ExprBV Symbol Symbol)] -> SubstV Symbol)
-> [[(Symbol, ExprBV Symbol Symbol)]] -> [SubstV Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, ExprBV Symbol Symbol)]
-> [[(Symbol, ExprBV Symbol Symbol)]]
forall a. [a] -> [[a]]
L.inits [(Symbol
x, Symbol -> ExprBV Symbol Symbol
forall b v. v -> ExprBV b v
F.EVar Symbol
y) | (Symbol
x, Symbol
y) <- [Symbol] -> [Symbol] -> [(Symbol, Symbol)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
ys0 [Symbol]
ys']
        ([Var]
αs, [Symbol]
ys')            = (Var -> Symbol) -> [Var] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol ([Var] -> [Symbol]) -> ([Var], [Var]) -> ([Var], [Symbol])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Var -> Bool) -> [Var] -> ([Var], [Var])
forall a. (a -> Bool) -> [a] -> ([a], [a])
L.partition Var -> Bool
isTyVar [Var]
ys
        tvs' :: [SpecType]
        tvs' :: [SpecType]
tvs'                 = Var -> SpecType
forall r c. IsReft r => Var -> RType c RTyVar r
rVar (Var -> SpecType) -> [Var] -> [SpecType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Var]
αs
        tvys :: [RTypeBV Symbol Symbol RTyCon RTyVar r]
tvys                 = Type -> RTypeBV Symbol Symbol RTyCon RTyVar r
forall r. IsReft r => Type -> RRType r
ofType (Type -> RTypeBV Symbol Symbol RTyCon RTyVar r)
-> (Var -> Type) -> Var -> RTypeBV Symbol Symbol RTyCon RTyVar r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> Type
varType (Var -> RTypeBV Symbol Symbol RTyCon RTyVar r)
-> [Var] -> [RTypeBV Symbol Symbol RTyCon RTyVar r]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Var]
αs

unfoldR SpecType
_  SpecType
_                [Var]
_  = Maybe SrcSpan -> [Char] -> (SpecType, [SpecType], SpecType)
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing [Char]
"Constraint.hs : unfoldR"

instantiateTys :: SpecType -> [SpecType] -> SpecType
instantiateTys :: SpecType -> [SpecType] -> SpecType
instantiateTys = (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
forall {r} {c} {tv} {b} {v}.
(IsReft r, TyConable c, FreeVar c tv,
 SubsTy tv (RTypeBV b v c tv (NoReftB b)) c,
 SubsTy tv (RTypeBV b v c tv (NoReftB b)) r,
 SubsTy tv (RTypeBV b v c tv (NoReftB b)) tv,
 SubsTy
   tv (RTypeBV b v c tv (NoReftB b)) (RTypeBV b v c tv (NoReftB b)),
 SubsTy
   tv
   (RTypeBV b v c tv (NoReftB b))
   (RTVar tv (RTypeBV b v c tv (NoReftB b))),
 Binder b, Hashable tv) =>
RTypeBV b v c tv r -> RTypeBV b v c tv r -> RTypeBV b v c tv r
go
  where
    go :: RTypeBV b v c tv r -> RTypeBV b v c tv r -> RTypeBV b v c tv r
go (RAllT RTVar tv (RTypeBV b v c tv (NoReftB b))
α RTypeBV b v c tv r
tbody r
_) RTypeBV b v c tv r
t = (tv, RTypeBV b v c tv r)
-> RTypeBV b v c tv r -> RTypeBV b v c tv r
forall tv r c b v.
(Eq tv, Hashable tv, IsReft r, TyConable c, Binder b,
 SubsTy tv (RTypeBV b v c tv (NoReftB b)) c,
 SubsTy tv (RTypeBV b v c tv (NoReftB b)) r,
 SubsTy
   tv (RTypeBV b v c tv (NoReftB b)) (RTypeBV b v c tv (NoReftB b)),
 FreeVar c tv, SubsTy tv (RTypeBV b v c tv (NoReftB b)) tv,
 SubsTy
   tv
   (RTypeBV b v c tv (NoReftB b))
   (RTVar tv (RTypeBV b v c tv (NoReftB b)))) =>
(tv, RTypeBV b v c tv r)
-> RTypeBV b v c tv r -> RTypeBV b v c tv r
subsTyVarMeet' (RTVar tv (RTypeBV b v c tv (NoReftB b)) -> tv
forall tv s. RTVar tv s -> tv
ty_var_value RTVar tv (RTypeBV b v c tv (NoReftB b))
α, RTypeBV b v c tv r
t) RTypeBV b v c tv r
tbody
    go RTypeBV b v c tv r
_ RTypeBV b v c tv r
_                 = Maybe SrcSpan -> [Char] -> RTypeBV b v c tv r
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing [Char]
"Constraint.instantiateTy"

instantiatePvs :: SpecType -> [SpecProp] -> SpecType
instantiatePvs :: SpecType -> [RTProp RTyCon RTyVar RReft] -> SpecType
instantiatePvs           = (SpecType -> RTProp RTyCon RTyVar RReft -> SpecType)
-> SpecType -> [RTProp RTyCon RTyVar RReft] -> 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 -> RTProp RTyCon RTyVar RReft -> SpecType
go
  where
    go :: SpecType -> RTProp RTyCon RTyVar RReft -> SpecType
go (RAllP PVarBV Symbol Symbol (RTypeBV Symbol Symbol RTyCon RTyVar NoReft)
p SpecType
tbody) RTProp RTyCon RTyVar RReft
r = [Char]
-> SpecType
-> [(PVarBV
       Symbol Symbol (RTypeBV Symbol Symbol RTyCon RTyVar NoReft),
     RTProp RTyCon RTyVar RReft)]
-> SpecType
replacePreds [Char]
"instantiatePv" SpecType
tbody [(PVarBV Symbol Symbol (RTypeBV Symbol Symbol RTyCon RTyVar NoReft)
p, RTProp RTyCon RTyVar RReft
r)]
    go SpecType
t               RTProp RTyCon RTyVar RReft
_ = [Char] -> [Char] -> SpecType
forall a. [Char] -> [Char] -> a
errorP [Char]
"" ([Char]
"Constraint.instantiatePvs: t = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SpecType -> [Char]
forall a. PPrint a => a -> [Char]
showpp SpecType
t)

checkTyCon :: (Outputable a) => (String, a) -> CGEnv -> SpecType -> SpecType
checkTyCon :: forall a.
Outputable a =>
([Char], a) -> CGEnv -> SpecType -> SpecType
checkTyCon ([Char], a)
_ CGEnv
_ t :: SpecType
t@RApp{} = SpecType
t
checkTyCon ([Char], a)
x CGEnv
g SpecType
t        = ([Char], a) -> CGEnv -> SpecType -> SpecType
forall a.
Outputable a =>
([Char], a) -> CGEnv -> SpecType -> SpecType
checkErr ([Char], a)
x CGEnv
g SpecType
t

checkFun :: (Outputable a) => (String, a) -> CGEnv -> SpecType -> SpecType
checkFun :: forall a.
Outputable a =>
([Char], a) -> CGEnv -> SpecType -> SpecType
checkFun ([Char], a)
_ CGEnv
_ t :: SpecType
t@RFun{} = SpecType
t
checkFun ([Char], a)
x CGEnv
g SpecType
t        = ([Char], a) -> CGEnv -> SpecType -> SpecType
forall a.
Outputable a =>
([Char], a) -> CGEnv -> SpecType -> SpecType
checkErr ([Char], a)
x CGEnv
g SpecType
t

checkAll :: (Outputable a) => (String, a) -> CGEnv -> SpecType -> SpecType
checkAll :: forall a.
Outputable a =>
([Char], a) -> CGEnv -> SpecType -> SpecType
checkAll ([Char], a)
_ CGEnv
_ t :: SpecType
t@RAllT{} = SpecType
t
checkAll ([Char], a)
x CGEnv
g SpecType
t         = ([Char], a) -> CGEnv -> SpecType -> SpecType
forall a.
Outputable a =>
([Char], a) -> CGEnv -> SpecType -> SpecType
checkErr ([Char], a)
x CGEnv
g SpecType
t

checkErr :: (Outputable a) => (String, a) -> CGEnv -> SpecType -> SpecType
checkErr :: forall a.
Outputable a =>
([Char], a) -> CGEnv -> SpecType -> SpecType
checkErr ([Char]
msg, a
e) CGEnv
γ SpecType
t = Maybe SrcSpan -> [Char] -> SpecType
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic (SrcSpan -> Maybe SrcSpan
forall a. a -> Maybe a
Just SrcSpan
sp) ([Char] -> SpecType) -> [Char] -> SpecType
forall a b. (a -> b) -> a -> b
$ [Char]
msg [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. Outputable a => a -> [Char]
GM.showPpr a
e [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
", type: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SpecType -> [Char]
forall a. PPrint a => a -> [Char]
showpp SpecType
t
  where
    sp :: SrcSpan
sp                = CGEnv -> SrcSpan
getLocation CGEnv
γ

varAnn :: CGEnv -> Var -> t -> Annot t
varAnn :: forall t. CGEnv -> Var -> t -> Annot t
varAnn CGEnv
γ Var
x t
t
  | Var
x Var -> HashSet Var -> Bool
forall a. Hashable a => a -> HashSet a -> Bool
`S.member` CGEnv -> HashSet Var
recs CGEnv
γ = SrcSpan -> Annot t
forall t. SrcSpan -> Annot t
AnnLoc (Var -> SrcSpan
forall a. NamedThing a => a -> SrcSpan
getSrcSpan Var
x)
  | Bool
otherwise           = t -> Annot t
forall t. t -> Annot t
AnnUse t
t

-----------------------------------------------------------------------
-- | Helpers: Creating Fresh Refinement -------------------------------
-----------------------------------------------------------------------
freshPredRef :: CGEnv -> CoreExpr -> PVar RSort -> CG SpecProp
freshPredRef :: CGEnv
-> Expr Var
-> PVarBV
     Symbol Symbol (RTypeBV Symbol Symbol RTyCon RTyVar NoReft)
-> CG (RTProp RTyCon RTyVar RReft)
freshPredRef CGEnv
γ Expr Var
e (PV Symbol
_ RTypeBV Symbol Symbol RTyCon RTyVar NoReft
rsort Symbol
_ [(RTypeBV Symbol Symbol RTyCon RTyVar NoReft, Symbol,
  ExprBV Symbol Symbol)]
as)
  = do t    <- Bool
-> KVKind -> Expr Var -> Type -> StateT CGInfo Identity SpecType
freshTyType (Config -> Bool
typeclass (CGEnv -> Config
forall t. HasConfig t => t -> Config
getConfig CGEnv
γ))  KVKind
PredInstE Expr Var
e (Bool -> RTypeBV Symbol Symbol RTyCon RTyVar NoReft -> Type
forall r. ToTypeable r => Bool -> RRType r -> Type
toType Bool
False RTypeBV Symbol Symbol RTyCon RTyVar NoReft
rsort)
       args <- mapM (const fresh) as
       let targs = [(Symbol
x, RTypeBV Symbol Symbol RTyCon RTyVar NoReft
s) | (Symbol
x, (RTypeBV Symbol Symbol RTyCon RTyVar NoReft
s, Symbol
y, ExprBV Symbol Symbol
z)) <- [Symbol]
-> [(RTypeBV Symbol Symbol RTyCon RTyVar NoReft, Symbol,
     ExprBV Symbol Symbol)]
-> [(Symbol,
     (RTypeBV Symbol Symbol RTyCon RTyVar NoReft, Symbol,
      ExprBV Symbol Symbol))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
args [(RTypeBV Symbol Symbol RTyCon RTyVar NoReft, Symbol,
  ExprBV Symbol Symbol)]
as, Symbol -> ExprBV Symbol Symbol
forall b v. v -> ExprBV b v
F.EVar Symbol
y ExprBV Symbol Symbol -> ExprBV Symbol Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== ExprBV Symbol Symbol
z ]
       γ' <- foldM (+=) γ [("freshPredRef", x, ofRSort τ) | (x, τ) <- targs]
       addW $ WfC γ' t
       return $ RProp targs t

--------------------------------------------------------------------------------
-- | Helpers: Creating Refinement Types For Various Things ---------------------
--------------------------------------------------------------------------------
argType :: Type -> Maybe F.Expr
argType :: Type -> Maybe (ExprBV Symbol Symbol)
argType (LitTy (NumTyLit Integer
i)) = Integer -> Maybe (ExprBV Symbol Symbol)
mkI Integer
i
argType (LitTy (StrTyLit FastString
s)) = ExprBV Symbol Symbol -> Maybe (ExprBV Symbol Symbol)
forall a. a -> Maybe a
Just (ExprBV Symbol Symbol -> Maybe (ExprBV Symbol Symbol))
-> ExprBV Symbol Symbol -> Maybe (ExprBV Symbol Symbol)
forall a b. (a -> b) -> a -> b
$ ByteString -> ExprBV Symbol Symbol
mkS (ByteString -> ExprBV Symbol Symbol)
-> ByteString -> ExprBV Symbol Symbol
forall a b. (a -> b) -> a -> b
$ FastString -> ByteString
bytesFS FastString
s
argType (TyVarTy Var
x)          = ExprBV Symbol Symbol -> Maybe (ExprBV Symbol Symbol)
forall a. a -> Maybe a
Just (ExprBV Symbol Symbol -> Maybe (ExprBV Symbol Symbol))
-> ExprBV Symbol Symbol -> Maybe (ExprBV Symbol Symbol)
forall a b. (a -> b) -> a -> b
$ Symbol -> ExprBV Symbol Symbol
forall b v. v -> ExprBV b v
F.EVar (Symbol -> ExprBV Symbol Symbol) -> Symbol -> ExprBV Symbol Symbol
forall a b. (a -> b) -> a -> b
$ Name -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (Name -> Symbol) -> Name -> Symbol
forall a b. (a -> b) -> a -> b
$ Var -> Name
varName Var
x
argType Type
t
  | [Char] -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (Type -> [Char]
forall a. Outputable a => a -> [Char]
GM.showPpr Type
t) Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
anyTypeSymbol
                             = ExprBV Symbol Symbol -> Maybe (ExprBV Symbol Symbol)
forall a. a -> Maybe a
Just (ExprBV Symbol Symbol -> Maybe (ExprBV Symbol Symbol))
-> ExprBV Symbol Symbol -> Maybe (ExprBV Symbol Symbol)
forall a b. (a -> b) -> a -> b
$ Symbol -> ExprBV Symbol Symbol
forall b v. v -> ExprBV b v
F.EVar Symbol
anyTypeSymbol
argType Type
_                    = Maybe (ExprBV Symbol Symbol)
forall a. Maybe a
Nothing


argExpr :: CGEnv -> CoreExpr -> Maybe F.Expr
argExpr :: CGEnv -> Expr Var -> Maybe (ExprBV Symbol Symbol)
argExpr CGEnv
_ (Var Var
v)          = ExprBV Symbol Symbol -> Maybe (ExprBV Symbol Symbol)
forall a. a -> Maybe a
Just (ExprBV Symbol Symbol -> Maybe (ExprBV Symbol Symbol))
-> ExprBV Symbol Symbol -> Maybe (ExprBV Symbol Symbol)
forall a b. (a -> b) -> a -> b
$ Var -> ExprBV Symbol Symbol
forall a. Symbolic a => a -> ExprBV Symbol Symbol
F.eVar Var
v
argExpr CGEnv
γ (Lit Literal
c)          = (Sort, Maybe (ExprBV Symbol Symbol))
-> Maybe (ExprBV Symbol Symbol)
forall a b. (a, b) -> b
snd ((Sort, Maybe (ExprBV Symbol Symbol))
 -> Maybe (ExprBV Symbol Symbol))
-> (Sort, Maybe (ExprBV Symbol Symbol))
-> Maybe (ExprBV Symbol Symbol)
forall a b. (a -> b) -> a -> b
$ TCEmb TyCon -> Literal -> (Sort, Maybe (ExprBV Symbol Symbol))
literalConst (CGEnv -> TCEmb TyCon
emb CGEnv
γ) Literal
c
argExpr CGEnv
γ (Tick CoreTickish
_ Expr Var
e)       = CGEnv -> Expr Var -> Maybe (ExprBV Symbol Symbol)
argExpr CGEnv
γ Expr Var
e
argExpr CGEnv
γ (App Expr Var
e (Type Type
_)) = CGEnv -> Expr Var -> Maybe (ExprBV Symbol Symbol)
argExpr CGEnv
γ Expr Var
e
argExpr CGEnv
_ Expr Var
_                = Maybe (ExprBV Symbol Symbol)
forall a. Maybe a
Nothing


lamExpr :: CGEnv -> CoreExpr -> CG (Maybe F.Expr)
lamExpr :: CGEnv -> Expr Var -> CG (Maybe (ExprBV Symbol Symbol))
lamExpr CGEnv
g Expr Var
e = do
    adts <- (CGInfo -> [DataDecl]) -> StateT CGInfo Identity [DataDecl]
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CGInfo -> [DataDecl]
cgADTs
    let dm = [DataDecl] -> DataConMap
dataConMap [DataDecl]
adts
    return $ eitherToMaybe $ runToLogic (emb g) mempty dm (getConfig g)
      (\[Char]
x -> Maybe SrcSpan -> [Char] -> Error
forall a. Maybe SrcSpan -> [Char] -> a
todo Maybe SrcSpan
forall a. Maybe a
Nothing ([Char]
"coreToLogic not working lamExpr: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
x))
      (coreToLogic e)

--------------------------------------------------------------------------------
(??=) :: (?callStack :: CallStack) => CGEnv -> Var -> CG SpecType
--------------------------------------------------------------------------------
CGEnv
γ ??= :: HasCallStack => CGEnv -> Var -> StateT CGInfo Identity SpecType
??= Var
x = case Symbol -> HashMap Symbol (Expr Var) -> Maybe (Expr Var)
forall k v. Hashable k => k -> HashMap k v -> Maybe v
M.lookup Symbol
x' (CGEnv -> HashMap Symbol (Expr Var)
lcb CGEnv
γ) of
            Just Expr Var
e  -> CGEnv -> Expr Var -> StateT CGInfo Identity SpecType
consE (CGEnv
γ CGEnv -> Symbol -> CGEnv
-= Symbol
x') Expr Var
e
            Maybe (Expr Var)
Nothing -> SpecType -> StateT CGInfo Identity SpecType
forall (m :: * -> *). FreshM m => SpecType -> m SpecType
refreshTy SpecType
tx
          where
            x' :: Symbol
x' = Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
x
            tx :: SpecType
tx = SpecType -> Maybe SpecType -> SpecType
forall a. a -> Maybe a -> a
fromMaybe SpecType
forall {r}. IsReft r => RRType r
tt (CGEnv
γ HasCallStack => CGEnv -> Symbol -> Maybe SpecType
CGEnv -> Symbol -> Maybe SpecType
?= Symbol
x')
            tt :: RRType r
tt = Type -> RRType r
forall r. IsReft r => Type -> RRType r
ofType (Type -> RRType r) -> Type -> RRType r
forall a b. (a -> b) -> a -> b
$ Var -> Type
varType Var
x


--------------------------------------------------------------------------------
varRefType :: (?callStack :: CallStack) => CGEnv -> Var -> CG SpecType
--------------------------------------------------------------------------------
varRefType :: HasCallStack => CGEnv -> Var -> StateT CGInfo Identity SpecType
varRefType CGEnv
γ Var
x =
  CGEnv -> Var -> SpecType -> SpecType
varRefType' CGEnv
γ Var
x (SpecType -> SpecType)
-> StateT CGInfo Identity SpecType
-> StateT CGInfo Identity SpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (CGEnv
γ HasCallStack => CGEnv -> Var -> StateT CGInfo Identity SpecType
CGEnv -> Var -> StateT CGInfo Identity SpecType
??= Var
x) -- F.tracepp (printf "varRefType x = [%s]" (showpp x))

varRefType' :: CGEnv -> Var -> SpecType -> SpecType
varRefType' :: CGEnv -> Var -> SpecType -> SpecType
varRefType' CGEnv
γ Var
x SpecType
t'
  | Just HashMap Symbol SpecType
tys <- CGEnv -> Maybe (HashMap Symbol SpecType)
trec CGEnv
γ, Just SpecType
tr  <- Symbol -> HashMap Symbol SpecType -> Maybe SpecType
forall k v. Hashable k => k -> HashMap k v -> Maybe v
M.lookup Symbol
x' HashMap Symbol SpecType
tys
  = SpecType -> RReft -> SpecType
forall {r} {c} {tv}.
(PPrint r, Meet r) =>
RType c tv r -> r -> RType c tv r
strengthen' SpecType
tr RReft
xr
  | Bool
otherwise
  = SpecType -> RReft -> SpecType
forall {r} {c} {tv}.
(PPrint r, Meet r) =>
RType c tv r -> r -> RType c tv r
strengthen' SpecType
t' RReft
xr
  where
    xr :: RReft
xr = Var -> RReft
forall a. Symbolic a => a -> RReft
singletonReft Var
x
    x' :: Symbol
x' = Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
x
    strengthen' :: RType c tv r -> r -> RType c tv r
strengthen' | CGEnv -> Bool
forall t. HasConfig t => t -> Bool
higherOrderFlag CGEnv
γ = RType c tv r -> r -> RType c tv r
forall {r} {c} {tv}.
(PPrint r, Meet r) =>
RType c tv r -> r -> RType c tv r
strengthenMeet
                | Bool
otherwise         = RType c tv r -> r -> RType c tv r
forall {r} {c} {tv}.
(PPrint r, Meet r) =>
RType c tv r -> r -> RType c tv r
strengthenTop

-- | create singleton types for function application
makeSingleton :: CGEnv -> CoreExpr -> SpecType -> SpecType
makeSingleton :: CGEnv -> Expr Var -> SpecType -> SpecType
makeSingleton CGEnv
γ Expr Var
cexpr SpecType
t
  | CGEnv -> Bool
forall t. HasConfig t => t -> Bool
higherOrderFlag CGEnv
γ, App Expr Var
f Expr Var
x <- Expr Var -> Expr Var
simplify Expr Var
cexpr
  = case (CGEnv -> Expr Var -> Maybe (ExprBV Symbol Symbol)
funExpr CGEnv
γ Expr Var
f, Expr Var -> Maybe (ExprBV Symbol Symbol)
argForAllExpr Expr Var
x) of
      (Just ExprBV Symbol Symbol
f', Just ExprBV Symbol Symbol
x')
                 | Bool -> Bool
not (if Config -> Bool
typeclass (CGEnv -> Config
forall t. HasConfig t => t -> Config
getConfig CGEnv
γ) then Expr Var -> Bool
GM.isEmbeddedDictExpr Expr Var
x else Expr Var -> Bool
GM.isPredExpr Expr Var
x) -- (isClassPred $ exprType x)
                 -> SpecType -> RReft -> SpecType
forall {r} {c} {tv}.
(PPrint r, Meet r) =>
RType c tv r -> r -> RType c tv r
strengthenMeet SpecType
t (ReftBV Symbol Symbol -> RReft
forall r v. r -> UReftV v r
uTop (ReftBV Symbol Symbol -> RReft) -> ReftBV Symbol Symbol -> RReft
forall a b. (a -> b) -> a -> b
$ ExprBV Symbol Symbol -> ReftBV Symbol Symbol
forall a. Expression a => a -> ReftBV Symbol Symbol
F.exprReft (ExprBV Symbol Symbol
-> ExprBV Symbol Symbol -> ExprBV Symbol Symbol
forall b v. ExprBV b v -> ExprBV b v -> ExprBV b v
F.EApp ExprBV Symbol Symbol
f' ExprBV Symbol Symbol
x'))
      (Just ExprBV Symbol Symbol
f', Just ExprBV Symbol Symbol
_)
                 -> SpecType -> RReft -> SpecType
forall {r} {c} {tv}.
(PPrint r, Meet r) =>
RType c tv r -> r -> RType c tv r
strengthenMeet SpecType
t (ReftBV Symbol Symbol -> RReft
forall r v. r -> UReftV v r
uTop (ReftBV Symbol Symbol -> RReft) -> ReftBV Symbol Symbol -> RReft
forall a b. (a -> b) -> a -> b
$ ExprBV Symbol Symbol -> ReftBV Symbol Symbol
forall a. Expression a => a -> ReftBV Symbol Symbol
F.exprReft ExprBV Symbol Symbol
f')
      (Maybe (ExprBV Symbol Symbol), Maybe (ExprBV Symbol Symbol))
_ -> SpecType
t
  | Config -> Bool
rankNTypes (CGEnv -> Config
forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)
  = case CGEnv -> Expr Var -> Maybe (ExprBV Symbol Symbol)
argExpr CGEnv
γ (Expr Var -> Expr Var
simplify Expr Var
cexpr) of
       Just ExprBV Symbol Symbol
e' -> SpecType -> RReft -> SpecType
forall {r} {c} {tv}.
(PPrint r, Meet r) =>
RType c tv r -> r -> RType c tv r
strengthenMeet SpecType
t (RReft -> SpecType) -> RReft -> SpecType
forall a b. (a -> b) -> a -> b
$ ReftBV Symbol Symbol -> RReft
forall r v. r -> UReftV v r
uTop (ExprBV Symbol Symbol -> ReftBV Symbol Symbol
forall a. Expression a => a -> ReftBV Symbol Symbol
F.exprReft ExprBV Symbol Symbol
e')
       Maybe (ExprBV Symbol Symbol)
_       -> SpecType
t
  | Bool
otherwise
  = SpecType
t
  where
    argForAllExpr :: Expr Var -> Maybe (ExprBV Symbol Symbol)
argForAllExpr (Var Var
x)
      | Config -> Bool
rankNTypes (CGEnv -> Config
forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)
      , Just ExprBV Symbol Symbol
e <- Var
-> HashMap Var (ExprBV Symbol Symbol)
-> Maybe (ExprBV Symbol Symbol)
forall k v. Hashable k => k -> HashMap k v -> Maybe v
M.lookup Var
x (CGEnv -> HashMap Var (ExprBV Symbol Symbol)
forallcb CGEnv
γ)
      = ExprBV Symbol Symbol -> Maybe (ExprBV Symbol Symbol)
forall a. a -> Maybe a
Just ExprBV Symbol Symbol
e
    argForAllExpr Expr Var
e
      = CGEnv -> Expr Var -> Maybe (ExprBV Symbol Symbol)
argExpr CGEnv
γ Expr Var
e



funExpr :: CGEnv -> CoreExpr -> Maybe F.Expr

funExpr :: CGEnv -> Expr Var -> Maybe (ExprBV Symbol Symbol)
funExpr CGEnv
_ (Var Var
v)
  = ExprBV Symbol Symbol -> Maybe (ExprBV Symbol Symbol)
forall a. a -> Maybe a
Just (ExprBV Symbol Symbol -> Maybe (ExprBV Symbol Symbol))
-> ExprBV Symbol Symbol -> Maybe (ExprBV Symbol Symbol)
forall a b. (a -> b) -> a -> b
$ Symbol -> ExprBV Symbol Symbol
forall b v. v -> ExprBV b v
F.EVar (Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
v)

funExpr CGEnv
γ (App Expr Var
e1 Expr Var
e2)
  = case (CGEnv -> Expr Var -> Maybe (ExprBV Symbol Symbol)
funExpr CGEnv
γ Expr Var
e1, CGEnv -> Expr Var -> Maybe (ExprBV Symbol Symbol)
argExpr CGEnv
γ Expr Var
e2) of
      (Just ExprBV Symbol Symbol
e1', Just ExprBV Symbol Symbol
e2') | Bool -> Bool
not (if Config -> Bool
typeclass (CGEnv -> Config
forall t. HasConfig t => t -> Config
getConfig CGEnv
γ) then Expr Var -> Bool
GM.isEmbeddedDictExpr Expr Var
e2
                                                             else Expr Var -> Bool
GM.isPredExpr Expr Var
e2) -- (isClassPred $ exprType e2)
                           -> ExprBV Symbol Symbol -> Maybe (ExprBV Symbol Symbol)
forall a. a -> Maybe a
Just (ExprBV Symbol Symbol
-> ExprBV Symbol Symbol -> ExprBV Symbol Symbol
forall b v. ExprBV b v -> ExprBV b v -> ExprBV b v
F.EApp ExprBV Symbol Symbol
e1' ExprBV Symbol Symbol
e2')
      (Just ExprBV Symbol Symbol
e1', Just ExprBV Symbol Symbol
_)   -> ExprBV Symbol Symbol -> Maybe (ExprBV Symbol Symbol)
forall a. a -> Maybe a
Just ExprBV Symbol Symbol
e1'
      (Maybe (ExprBV Symbol Symbol), Maybe (ExprBV Symbol Symbol))
_                    -> Maybe (ExprBV Symbol Symbol)
forall a. Maybe a
Nothing

funExpr CGEnv
_ Expr Var
_
  = Maybe (ExprBV Symbol Symbol)
forall a. Maybe a
Nothing

simplify :: CoreExpr -> CoreExpr
simplify :: Expr Var -> Expr Var
simplify (Tick CoreTickish
_ Expr Var
e)            = Expr Var -> Expr Var
simplify Expr Var
e
simplify (App Expr Var
e (Type Type
_))      = Expr Var -> Expr Var
simplify Expr Var
e
simplify (App Expr Var
e1 Expr Var
e2)           = Expr Var -> Expr Var -> Expr Var
forall b. Expr b -> Expr b -> Expr b
App (Expr Var -> Expr Var
simplify Expr Var
e1) (Expr Var -> Expr Var
simplify Expr Var
e2)
simplify (Lam Var
x Expr Var
e) | Var -> Bool
isTyVar Var
x = Expr Var -> Expr Var
simplify Expr Var
e
simplify Expr Var
e                     = Expr Var
e


singletonReft :: (F.Symbolic a) => a -> UReft F.Reft
singletonReft :: forall a. Symbolic a => a -> RReft
singletonReft = ReftBV Symbol Symbol -> RReft
forall r v. r -> UReftV v r
uTop (ReftBV Symbol Symbol -> RReft)
-> (a -> ReftBV Symbol Symbol) -> a -> RReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> ReftBV Symbol Symbol
forall a. Symbolic a => a -> ReftBV Symbol Symbol
F.symbolReft (Symbol -> ReftBV Symbol Symbol)
-> (a -> Symbol) -> a -> ReftBV Symbol Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol

-- | RJ: `nomeet` replaces `strengthenS` for `strengthen` in the definition
--   of `varRefType`. Why does `tests/neg/strata.hs` fail EVEN if I just replace
--   the `otherwise` case? The fq file holds no answers, both are sat.
strengthenTop :: (PPrint r, Meet r) => RType c tv r -> r -> RType c tv r
strengthenTop :: forall {r} {c} {tv}.
(PPrint r, Meet r) =>
RType c tv r -> r -> RType c tv r
strengthenTop (RApp c
c [RTypeBV Symbol Symbol c tv r]
ts [RTPropBV Symbol Symbol c tv r]
rs r
r) r
r'   = c
-> [RTypeBV Symbol Symbol c tv r]
-> [RTPropBV Symbol Symbol c tv r]
-> r
-> RTypeBV Symbol Symbol c tv r
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 c
c [RTypeBV Symbol Symbol c tv r]
ts [RTPropBV Symbol Symbol c tv r]
rs   (r -> RTypeBV Symbol Symbol c tv r)
-> r -> RTypeBV Symbol Symbol c tv r
forall a b. (a -> b) -> a -> b
$ r -> r -> r
forall r. Meet r => r -> r -> r
meet r
r r
r'
strengthenTop (RVar tv
a r
r) r
r'         = tv -> r -> RTypeBV Symbol Symbol c tv r
forall b v c tv r. tv -> r -> RTypeBV b v c tv r
RVar tv
a         (r -> RTypeBV Symbol Symbol c tv r)
-> r -> RTypeBV Symbol Symbol c tv r
forall a b. (a -> b) -> a -> b
$ r -> r -> r
forall r. Meet r => r -> r -> r
meet r
r r
r'
strengthenTop (RFun Symbol
b RFInfo
i RTypeBV Symbol Symbol c tv r
t1 RTypeBV Symbol Symbol c tv r
t2 r
r) r
r' = Symbol
-> RFInfo
-> RTypeBV Symbol Symbol c tv r
-> RTypeBV Symbol Symbol c tv r
-> r
-> RTypeBV Symbol Symbol c tv r
forall b v c tv r.
b
-> RFInfo
-> RTypeBV b v c tv r
-> RTypeBV b v c tv r
-> r
-> RTypeBV b v c tv r
RFun Symbol
b RFInfo
i RTypeBV Symbol Symbol c tv r
t1 RTypeBV Symbol Symbol c tv r
t2 (r -> RTypeBV Symbol Symbol c tv r)
-> r -> RTypeBV Symbol Symbol c tv r
forall a b. (a -> b) -> a -> b
$ r -> r -> r
forall r. Meet r => r -> r -> r
meet r
r r
r'
strengthenTop (RAppTy RTypeBV Symbol Symbol c tv r
t1 RTypeBV Symbol Symbol c tv r
t2 r
r) r
r'   = RTypeBV Symbol Symbol c tv r
-> RTypeBV Symbol Symbol c tv r
-> r
-> RTypeBV Symbol Symbol c tv r
forall b v c tv r.
RTypeBV b v c tv r -> RTypeBV b v c tv r -> r -> RTypeBV b v c tv r
RAppTy RTypeBV Symbol Symbol c tv r
t1 RTypeBV Symbol Symbol c tv r
t2   (r -> RTypeBV Symbol Symbol c tv r)
-> r -> RTypeBV Symbol Symbol c tv r
forall a b. (a -> b) -> a -> b
$ r -> r -> r
forall r. Meet r => r -> r -> r
meet r
r r
r'
strengthenTop (RAllT RTVUBV Symbol Symbol c tv
a RTypeBV Symbol Symbol c tv r
t r
r)    r
r'   = RTVUBV Symbol Symbol c tv
-> RTypeBV Symbol Symbol c tv r
-> r
-> RTypeBV Symbol Symbol c tv r
forall b v c tv r.
RTVUBV b v c tv -> RTypeBV b v c tv r -> r -> RTypeBV b v c tv r
RAllT RTVUBV Symbol Symbol c tv
a RTypeBV Symbol Symbol c tv r
t      (r -> RTypeBV Symbol Symbol c tv r)
-> r -> RTypeBV Symbol Symbol c tv r
forall a b. (a -> b) -> a -> b
$ r -> r -> r
forall r. Meet r => r -> r -> r
meet r
r r
r'
strengthenTop RTypeBV Symbol Symbol c tv r
t r
_                   = RTypeBV Symbol Symbol c tv r
t

-- TODO: this is almost identical to RT.strengthen! merge them!
strengthenMeet :: (PPrint r, Meet r) => RType c tv r -> r -> RType c tv r
strengthenMeet :: forall {r} {c} {tv}.
(PPrint r, Meet r) =>
RType c tv r -> r -> RType c tv r
strengthenMeet (RApp c
c [RTypeBV Symbol Symbol c tv r]
ts [RTPropBV Symbol Symbol c tv r]
rs r
r) r
r'  = c
-> [RTypeBV Symbol Symbol c tv r]
-> [RTPropBV Symbol Symbol c tv r]
-> r
-> RTypeBV Symbol Symbol c tv r
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 c
c [RTypeBV Symbol Symbol c tv r]
ts [RTPropBV Symbol Symbol c tv r]
rs (r
r r -> r -> r
forall r. Meet r => r -> r -> r
`meet` r
r')
strengthenMeet (RVar tv
a r
r) r
r'        = tv -> r -> RTypeBV Symbol Symbol c tv r
forall b v c tv r. tv -> r -> RTypeBV b v c tv r
RVar tv
a       (r
r r -> r -> r
forall r. Meet r => r -> r -> r
`meet` r
r')
strengthenMeet (RFun Symbol
b RFInfo
i RTypeBV Symbol Symbol c tv r
t1 RTypeBV Symbol Symbol c tv r
t2 r
r) r
r'= Symbol
-> RFInfo
-> RTypeBV Symbol Symbol c tv r
-> RTypeBV Symbol Symbol c tv r
-> r
-> RTypeBV Symbol Symbol c tv r
forall b v c tv r.
b
-> RFInfo
-> RTypeBV b v c tv r
-> RTypeBV b v c tv r
-> r
-> RTypeBV b v c tv r
RFun Symbol
b RFInfo
i RTypeBV Symbol Symbol c tv r
t1 RTypeBV Symbol Symbol c tv r
t2 (r
r r -> r -> r
forall r. Meet r => r -> r -> r
`meet` r
r')
strengthenMeet (RAppTy RTypeBV Symbol Symbol c tv r
t1 RTypeBV Symbol Symbol c tv r
t2 r
r) r
r'  = RTypeBV Symbol Symbol c tv r
-> RTypeBV Symbol Symbol c tv r
-> r
-> RTypeBV Symbol Symbol c tv r
forall b v c tv r.
RTypeBV b v c tv r -> RTypeBV b v c tv r -> r -> RTypeBV b v c tv r
RAppTy RTypeBV Symbol Symbol c tv r
t1 RTypeBV Symbol Symbol c tv r
t2 (r
r r -> r -> r
forall r. Meet r => r -> r -> r
`meet` r
r')
strengthenMeet (RAllT RTVUBV Symbol Symbol c tv
a RTypeBV Symbol Symbol c tv r
t r
r) r
r'     = RTVUBV Symbol Symbol c tv
-> RTypeBV Symbol Symbol c tv r
-> r
-> RTypeBV Symbol Symbol c tv r
forall b v c tv r.
RTVUBV b v c tv -> RTypeBV b v c tv r -> r -> RTypeBV b v c tv r
RAllT RTVUBV Symbol Symbol c tv
a (RTypeBV Symbol Symbol c tv r -> r -> RTypeBV Symbol Symbol c tv r
forall {r} {c} {tv}.
(PPrint r, Meet r) =>
RType c tv r -> r -> RType c tv r
strengthenMeet RTypeBV Symbol Symbol c tv r
t r
r') (r
r r -> r -> r
forall r. Meet r => r -> r -> r
`meet` r
r')
strengthenMeet RTypeBV Symbol Symbol c tv r
t r
_                  = RTypeBV Symbol Symbol c tv r
t

--------------------------------------------------------------------------------
-- | Cleaner Signatures For Rec-bindings ---------------------------------------
--------------------------------------------------------------------------------
exprLoc                         :: CoreExpr -> Maybe SrcSpan
exprLoc :: Expr Var -> Maybe SrcSpan
exprLoc (Tick CoreTickish
tt Expr Var
_)             = SrcSpan -> Maybe SrcSpan
forall a. a -> Maybe a
Just (SrcSpan -> Maybe SrcSpan) -> SrcSpan -> Maybe SrcSpan
forall a b. (a -> b) -> a -> b
$ CoreTickish -> SrcSpan
GM.tickSrcSpan CoreTickish
tt
exprLoc (App Expr Var
e Expr Var
a) | Expr Var -> Bool
isType Expr Var
a    = Expr Var -> Maybe SrcSpan
exprLoc Expr Var
e
exprLoc Expr Var
_                       = Maybe SrcSpan
forall a. Maybe a
Nothing

isType :: Expr CoreBndr -> Bool
isType :: Expr Var -> Bool
isType (Type Type
_)                 = Bool
True
isType Expr Var
a                        = HasCallStack => Type -> Type -> Bool
Type -> Type -> Bool
eqType (HasDebugCallStack => Expr Var -> Type
Expr Var -> Type
exprType Expr Var
a) Type
predType

-- | @isGenericVar@ determines whether the @RTyVar@ has no class constraints
isGenericVar :: RTyVar -> SpecType -> Bool
isGenericVar :: RTyVar -> SpecType -> Bool
isGenericVar RTyVar
α SpecType
st =  ((Class, RTyVar) -> Bool) -> [(Class, RTyVar)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\(Class
c, RTyVar
α') -> (RTyVar
α'RTyVar -> RTyVar -> Bool
forall a. Eq a => a -> a -> Bool
/=RTyVar
α) Bool -> Bool -> Bool
|| Class -> Bool
isGenericClass Class
c ) (SpecType -> [(Class, RTyVar)]
forall {r} {b}.
(ReftBind r ~ Symbol, PPrint b, PPrint r, PPrint (ReftVar r),
 Fixpoint (ReftVar r), ToReft r, Ord (ReftVar r), Hashable b) =>
RTypeBV Symbol Symbol RTyCon b r -> [(Class, b)]
classConstrs SpecType
st)
  where
    classConstrs :: RTypeBV Symbol Symbol RTyCon b r -> [(Class, b)]
classConstrs RTypeBV Symbol Symbol RTyCon b r
t = [(Class
c, RTVar b (RTypeV Symbol RTyCon b NoReft) -> b
forall tv s. RTVar tv s -> tv
ty_var_value RTVar b (RTypeV Symbol RTyCon b NoReft)
α')
                        | (Class
c, [RTypeBV Symbol Symbol RTyCon b r]
ts) <- RTypeBV Symbol Symbol RTyCon b r
-> [(Class, [RTypeBV Symbol Symbol RTyCon b r])]
forall tv r.
OkRT RTyCon tv r =>
RType RTyCon tv r -> [(Class, [RType RTyCon tv r])]
tyClasses RTypeBV Symbol Symbol RTyCon b r
t
                        , RTypeBV Symbol Symbol RTyCon b r
t'      <- [RTypeBV Symbol Symbol RTyCon b r]
ts
                        , RTVar b (RTypeV Symbol RTyCon b NoReft)
α'      <- RTypeBV Symbol Symbol RTyCon b r
-> [RTVar b (RTypeV Symbol RTyCon b NoReft)]
forall tv v c r.
Eq tv =>
RTypeV v c tv r -> [RTVar tv (RTypeV v c tv NoReft)]
freeTyVars RTypeBV Symbol Symbol RTyCon b r
t']
    isGenericClass :: Class -> Bool
isGenericClass Class
c = Class -> Name
className Class
c Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name
ordClassName, Name
eqClassName] -- , functorClassName, monadClassName]

-- instance MonadFail CG where
--  fail msg = panic Nothing msg

instance MonadFail Data.Functor.Identity.Identity where
  fail :: forall a. HasCallStack => [Char] -> Identity a
fail [Char]
msg = Maybe SrcSpan -> [Char] -> Identity a
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing [Char]
msg