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

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

-- | 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, generateConstraintsWithEnv, 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.State
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, mapSnd, 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 hiding (binds, Loc, loc, Def)
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.Transforms.CoreToLogic (weakenResult, runToLogic, coreToLogic)
import           Language.Haskell.Liquid.Bare.DataType (dataConMap, makeDataConChecker)

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

generateConstraintsWithEnv :: TargetInfo -> CGInfo -> CGEnv -> CGInfo
--------------------------------------------------------------------------------
generateConstraintsWithEnv :: TargetInfo -> CGInfo -> CGEnv -> CGInfo
generateConstraintsWithEnv TargetInfo
info CGInfo
cgi CGEnv
γ = {-# SCC "ConsGenEnv" #-} forall s a. State s a -> s -> s
execState StateT CGInfo Identity ()
act CGInfo
cgi
  where
    act :: StateT CGInfo Identity ()
act                  = CGEnv -> Config -> TargetInfo -> StateT CGInfo Identity ()
consAct CGEnv
γ Config
cfg TargetInfo
info
    cfg :: Config
cfg                  = forall t. HasConfig t => t -> Config
getConfig   TargetInfo
info

consAct :: CGEnv -> Config -> TargetInfo -> CG ()
consAct :: CGEnv -> Config -> TargetInfo -> StateT CGInfo Identity ()
consAct CGEnv
γ Config
cfg TargetInfo
info = do
  let sSpc :: GhcSpecSig
sSpc = TargetSpec -> GhcSpecSig
gsSig forall b c a. (b -> c) -> (a -> b) -> a -> c
. TargetInfo -> TargetSpec
giSpec forall a b. (a -> b) -> a -> b
$ TargetInfo
info
  let gSrc :: TargetSrc
gSrc = TargetInfo -> TargetSrc
giSrc TargetInfo
info
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Config -> Bool
gradual Config
cfg) (forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (WfC -> StateT CGInfo Identity ()
addW forall b c a. (b -> c) -> (a -> b) -> a -> c
. CGEnv -> SpecType -> WfC
WfC CGEnv
γ forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Located a -> a
val forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) (GhcSpecSig -> [(Id, Located SpecType)]
gsTySigs GhcSpecSig
sSpc forall a. [a] -> [a] -> [a]
++ GhcSpecSig -> [(Id, Located SpecType)]
gsAsmSigs GhcSpecSig
sSpc))
  CGEnv
γ' <- forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (Config -> TargetInfo -> CGEnv -> CoreBind -> CG CGEnv
consCBTop Config
cfg TargetInfo
info) CGEnv
γ (TargetSrc -> [CoreBind]
giCbs TargetSrc
gSrc)
  -- Relational Checking: the following only runs when the list of relational specs is not empty
  (PrEnv
ψ, CGEnv
γ'') <- forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (Config
-> TargetInfo
-> (PrEnv, CGEnv)
-> (Id, Id, Located SpecType, Located SpecType, RelExpr, RelExpr)
-> CG (PrEnv, CGEnv)
consAssmRel Config
cfg TargetInfo
info) ([], CGEnv
γ') (GhcSpecSig
-> [(Id, Id, Located SpecType, Located SpecType, RelExpr, RelExpr)]
gsAsmRel GhcSpecSig
sSpc forall a. [a] -> [a] -> [a]
++ GhcSpecSig
-> [(Id, Id, Located SpecType, Located SpecType, RelExpr, RelExpr)]
gsRelation GhcSpecSig
sSpc)
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Config
-> TargetInfo
-> CGEnv
-> PrEnv
-> (Id, Id, Located SpecType, Located SpecType, RelExpr, RelExpr)
-> StateT CGInfo Identity ()
consRelTop Config
cfg TargetInfo
info CGEnv
γ'' PrEnv
ψ) (GhcSpecSig
-> [(Id, Id, Located SpecType, Located SpecType, RelExpr, RelExpr)]
gsRelation GhcSpecSig
sSpc)
  -- End: Relational Checking
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (CGEnv
-> (Id, MethodType (Located SpecType)) -> StateT CGInfo Identity ()
consClass CGEnv
γ) (GhcSpecSig -> [(Id, MethodType (Located SpecType))]
gsMethods forall a b. (a -> b) -> a -> b
$ TargetSpec -> GhcSpecSig
gsSig forall a b. (a -> b) -> a -> b
$ TargetInfo -> TargetSpec
giSpec TargetInfo
info)
  [SubC]
hcs <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CGInfo -> [SubC]
hsCs
  [WfC]
hws <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CGInfo -> [WfC]
hsWfs
  [FixSubC]
fcs <- forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Bool -> SubC -> StateT CGInfo Identity [FixSubC]
splitC (Config -> Bool
typeclass (forall t. HasConfig t => t -> Config
getConfig TargetInfo
info))) [SubC]
hcs
  [FixWfC]
fws <- forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM WfC -> StateT CGInfo Identity [FixWfC]
splitW [WfC]
hws
  forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \CGInfo
st -> CGInfo
st { fEnv :: SEnv Sort
fEnv     = CGInfo -> SEnv Sort
fEnv    CGInfo
st forall a. Monoid a => a -> a -> a
`mappend` FEnv -> SEnv Sort
feEnv (CGEnv -> FEnv
fenv CGEnv
γ)
                     , cgLits :: SEnv Sort
cgLits   = CGEnv -> SEnv Sort
litEnv   CGEnv
γ
                     , cgConsts :: SEnv Sort
cgConsts = CGInfo -> SEnv Sort
cgConsts CGInfo
st forall a. Monoid a => a -> a -> a
`mappend` CGEnv -> SEnv Sort
constEnv CGEnv
γ
                     , fixCs :: [FixSubC]
fixCs    = [FixSubC]
fcs
                     , fixWfs :: [FixWfC]
fixWfs   = [FixWfC]
fws }

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

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

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

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

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

--------------------------------------------------------------------------------
consCB :: TCheck -> CGEnv -> CoreBind -> CG CGEnv
--------------------------------------------------------------------------------
-- do termination checking
consCB :: TCheck -> CGEnv -> CoreBind -> CG CGEnv
consCB TCheck
TerminationCheck CGEnv
γ (Rec [(Id, CoreExpr)]
xes)
  = do HashMap Id [Located Expr]
texprs <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CGInfo -> HashMap Id [Located Expr]
termExprs
       forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \CGInfo
i -> CGInfo
i { recCount :: Int
recCount = CGInfo -> Int
recCount CGInfo
i forall a. Num a => a -> a -> a
+ forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Id, CoreExpr)]
xes }
       let xxes :: [(Id, [Located Expr])]
xxes = forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (forall {k} {a}. Hashable k => k -> HashMap k a -> Maybe (k, a)
`lookup'` HashMap Id [Located Expr]
texprs) [Id]
xs
       if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Id, [Located Expr])]
xxes
         then (Bool
 -> CGEnv
 -> (Id, CoreExpr, Template SpecType)
 -> CG (Template SpecType))
-> CGEnv -> [(Id, CoreExpr)] -> CG CGEnv
consCBSizedTys Bool
-> CGEnv
-> (Id, CoreExpr, Template SpecType)
-> CG (Template SpecType)
consBind CGEnv
γ [(Id, CoreExpr)]
xes
         else forall {t :: * -> *} {a} {p}. Foldable t => t a -> p -> p
check [(Id, [Located Expr])]
xxes forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Bool
 -> CGEnv
 -> (Id, CoreExpr, Template SpecType)
 -> CG (Template SpecType))
-> CGEnv -> [(Id, CoreExpr)] -> CG CGEnv
consCBWithExprs Bool
-> CGEnv
-> (Id, CoreExpr, Template SpecType)
-> CG (Template SpecType)
consBind CGEnv
γ [(Id, CoreExpr)]
xes
    where
      xs :: [Id]
xs = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Id, CoreExpr)]
xes
      check :: t a -> p -> p
check t a
ys p
r | forall (t :: * -> *) a. Foldable t => t a -> Int
length t a
ys forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length [Id]
xs = p
r
                 | Bool
otherwise              = forall a. Maybe SrcSpan -> [Char] -> a
panic (forall a. a -> Maybe a
Just SrcSpan
loc) forall {a}. IsString a => a
msg
      msg :: a
msg        = a
"Termination expressions must be provided for all mutually recursive binders"
      loc :: SrcSpan
loc        = forall a. NamedThing a => a -> SrcSpan
getSrcSpan (forall a. [a] -> a
head [Id]
xs)
      lookup' :: k -> HashMap k a -> Maybe (k, a)
lookup' k
k HashMap k a
m = (k
k,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall k v. (Eq k, 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 [(Id, CoreExpr)]
xes)
  = do [(Id, CoreExpr, Template SpecType)]
xets     <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Id, CoreExpr)]
xes forall a b. (a -> b) -> a -> b
$ \(Id
x, CoreExpr
e) -> (Id
x, CoreExpr
e,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CGEnv -> (Id, Maybe CoreExpr) -> CG (Template SpecType)
varTemplate CGEnv
γ (Id
x, forall a. a -> Maybe a
Just CoreExpr
e)
       forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify     forall a b. (a -> b) -> a -> b
$ \CGInfo
i -> CGInfo
i { recCount :: Int
recCount = CGInfo -> Int
recCount CGInfo
i forall a. Num a => a -> a -> a
+ forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Id, CoreExpr)]
xes }
       let xts :: [(Id, Template SpecType)]
xts    = [(Id
x, Template SpecType
to) | (Id
x, CoreExpr
_, Template SpecType
to) <- [(Id, CoreExpr, Template SpecType)]
xets]
       CGEnv
γ'        <- forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM forall a. Symbolic a => CGEnv -> (a, Template SpecType) -> CG CGEnv
extender (CGEnv
γ CGEnv -> [Id] -> CGEnv
`setRecs` (forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Id, Template SpecType)]
xts)) [(Id, Template SpecType)]
xts
       forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Bool
-> CGEnv
-> (Id, CoreExpr, Template SpecType)
-> CG (Template SpecType)
consBind Bool
True CGEnv
γ') [(Id, CoreExpr, Template SpecType)]
xets
       forall (m :: * -> *) a. Monad m => a -> m a
return CGEnv
γ'

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

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

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

consCB TCheck
_ CGEnv
γ (NonRec Id
x CoreExpr
e)
  = do Template SpecType
to  <- CGEnv -> (Id, Maybe CoreExpr) -> CG (Template SpecType)
varTemplate CGEnv
γ (Id
x, forall a. Maybe a
Nothing)
       Template SpecType
to' <- Bool
-> CGEnv
-> (Id, CoreExpr, Template SpecType)
-> CG (Template SpecType)
consBind Bool
False CGEnv
γ (Id
x, CoreExpr
e, Template SpecType
to) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= CGEnv -> Template SpecType -> CG (Template SpecType)
addPostTemplate CGEnv
γ
       forall a. Symbolic a => CGEnv -> (a, Template SpecType) -> CG CGEnv
extender CGEnv
γ (Id
x, CGEnv -> CoreExpr -> SpecType -> SpecType
makeSingleton CGEnv
γ (CoreExpr -> CoreExpr
simplify CoreExpr
e) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Template SpecType
to')

grepDictionary :: CoreExpr -> Maybe (Var, [Type])
grepDictionary :: CoreExpr -> Maybe (Id, [Type])
grepDictionary = forall {b}. [Type] -> Expr b -> Maybe (Id, [Type])
go []
  where
    go :: [Type] -> Expr b -> Maybe (Id, [Type])
go [Type]
ts (App (Var Id
w) (Type Type
t)) = forall a. a -> Maybe a
Just (Id
w, forall a. [a] -> [a]
reverse (Type
tforall a. a -> [a] -> [a]
:[Type]
ts))
    go [Type]
ts (App Expr b
e (Type Type
t))       = [Type] -> Expr b -> Maybe (Id, [Type])
go (Type
tforall a. a -> [a] -> [a]
:[Type]
ts) Expr b
e
    go [Type]
ts (App Expr b
e (Var Id
_))        = [Type] -> Expr b -> Maybe (Id, [Type])
go [Type]
ts Expr b
e
    go [Type]
ts (Let Bind b
_ Expr b
e)              = [Type] -> Expr b -> Maybe (Id, [Type])
go [Type]
ts Expr b
e
    go [Type]
_ Expr b
_                       = forall a. Maybe a
Nothing

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

consBind Bool
isRec' CGEnv
γ (Id
x, CoreExpr
e, Asserted SpecType
spect)
  = do let γ' :: CGEnv
γ'       = CGEnv
γ CGEnv -> Id -> CGEnv
`setBind` Id
x
           ([(RTVar RTyVar (RType RTyCon RTyVar ()), RReft)]
_,[PVar (RType RTyCon RTyVar ())]
πs,SpecType
_) = forall tv c r.
RType tv c r
-> ([(RTVar c (RType tv c ()), r)], [PVar (RType tv c ())],
    RType tv c r)
bkUniv SpecType
spect
       CGEnv
cgenv    <- forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM CGEnv -> PVar (RType RTyCon RTyVar ()) -> CG CGEnv
addPToEnv CGEnv
γ' [PVar (RType RTyCon RTyVar ())]
πs
       CGEnv -> CoreExpr -> SpecType -> StateT CGInfo Identity ()
cconsE CGEnv
cgenv CoreExpr
e (Bool -> Id -> SpecType -> SpecType
weakenResult (Config -> Bool
typeclass (forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)) Id
x SpecType
spect)
       forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall a. Symbolic a => a -> Symbol
F.symbol Id
x Symbol -> HEnv -> Bool
`elemHEnv` CGEnv -> HEnv
holes CGEnv
γ) forall a b. (a -> b) -> a -> b
$
         -- have to add the wf constraint here for HOLEs so we have the proper env
         WfC -> StateT CGInfo Identity ()
addW forall a b. (a -> b) -> a -> b
$ CGEnv -> SpecType -> WfC
WfC CGEnv
cgenv forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap RReft -> RReft
killSubst SpecType
spect
       Id -> Annot SpecType -> StateT CGInfo Identity ()
addIdA Id
x (forall t. Bool -> t -> Annot t
defAnn Bool
isRec' SpecType
spect)
       forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Template a
Asserted SpecType
spect

consBind Bool
isRec' CGEnv
γ (Id
x, CoreExpr
e, Internal SpecType
spect)
  = do let γ' :: CGEnv
γ'       = CGEnv
γ CGEnv -> Id -> CGEnv
`setBind` Id
x
           ([(RTVar RTyVar (RType RTyCon RTyVar ()), RReft)]
_,[PVar (RType RTyCon RTyVar ())]
πs,SpecType
_) = forall tv c r.
RType tv c r
-> ([(RTVar c (RType tv c ()), r)], [PVar (RType tv c ())],
    RType tv c r)
bkUniv SpecType
spect
       CGEnv
γπ    <- forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM CGEnv -> PVar (RType RTyCon RTyVar ()) -> CG CGEnv
addPToEnv CGEnv
γ' [PVar (RType RTyCon RTyVar ())]
πs
       let γπ' :: CGEnv
γπ' = CGEnv
γπ {cerr :: Maybe (TError SpecType)
cerr = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall t. SrcSpan -> Doc -> Doc -> TError t
ErrHMeas (CGEnv -> SrcSpan
getLocation CGEnv
γπ) (forall a. PPrint a => a -> Doc
pprint Id
x) ([Char] -> Doc
text forall {a}. IsString a => a
explanation)}
       CGEnv -> CoreExpr -> SpecType -> StateT CGInfo Identity ()
cconsE CGEnv
γπ' CoreExpr
e SpecType
spect
       forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall a. Symbolic a => a -> Symbol
F.symbol Id
x Symbol -> HEnv -> Bool
`elemHEnv` CGEnv -> HEnv
holes CGEnv
γ) forall a b. (a -> b) -> a -> b
$
         -- have to add the wf constraint here for HOLEs so we have the proper env
         WfC -> StateT CGInfo Identity ()
addW forall a b. (a -> b) -> a -> b
$ CGEnv -> SpecType -> WfC
WfC CGEnv
γπ forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap RReft -> RReft
killSubst SpecType
spect
       Id -> Annot SpecType -> StateT CGInfo Identity ()
addIdA Id
x (forall t. Bool -> t -> Annot t
defAnn Bool
isRec' SpecType
spect)
       forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Template a
Internal SpecType
spect
  where
    explanation :: a
explanation = a
"Cannot give singleton type to the function definition."

consBind Bool
isRec' CGEnv
γ (Id
x, CoreExpr
e, Assumed SpecType
spect)
  = do let γ' :: CGEnv
γ' = CGEnv
γ CGEnv -> Id -> CGEnv
`setBind` Id
x
       CGEnv
γπ    <- forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM CGEnv -> PVar (RType RTyCon RTyVar ()) -> CG CGEnv
addPToEnv CGEnv
γ' [PVar (RType RTyCon RTyVar ())]
πs
       CGEnv -> CoreExpr -> SpecType -> StateT CGInfo Identity ()
cconsE CGEnv
γπ CoreExpr
e forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) a. Freshable m a => Bool -> a -> m a
true (Config -> Bool
typeclass (forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)) SpecType
spect
       Id -> Annot SpecType -> StateT CGInfo Identity ()
addIdA Id
x (forall t. Bool -> t -> Annot t
defAnn Bool
isRec' SpecType
spect)
       forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Template a
Asserted SpecType
spect
    where πs :: [PVar (RType RTyCon RTyVar ())]
πs   = forall c tv r. RTypeRep c tv r -> [PVar (RType c tv ())]
ty_preds forall a b. (a -> b) -> a -> b
$ forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep SpecType
spect

consBind Bool
isRec' CGEnv
γ (Id
x, CoreExpr
e, Template SpecType
Unknown)
  = do SpecType
t'    <- CGEnv -> CoreExpr -> CG SpecType
consE (CGEnv
γ CGEnv -> Id -> CGEnv
`setBind` Id
x) CoreExpr
e
       SpecType
t     <- Id -> SpecType -> CG SpecType
topSpecType Id
x SpecType
t'
       Id -> Annot SpecType -> StateT CGInfo Identity ()
addIdA Id
x (forall t. Bool -> t -> Annot t
defAnn Bool
isRec' SpecType
t)
       forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Id -> Bool
GM.isExternalId Id
x) (forall a. PPrint a => a -> SpecType -> StateT CGInfo Identity ()
addKuts Id
x SpecType
t)
       forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Template a
Asserted SpecType
t

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

killSubstReft :: F.Reft -> F.Reft
killSubstReft :: Reft -> Reft
killSubstReft = forall t a ctx.
(Visitable t, Monoid a) =>
Visitor a ctx -> ctx -> a -> t -> t
trans forall {acc} {ctx}. Monoid acc => Visitor acc ctx
kv () ()
  where
    kv :: Visitor acc ctx
kv    = forall {acc} {ctx}. Monoid acc => Visitor acc ctx
defaultVisitor { txExpr :: ctx -> Expr -> Expr
txExpr = forall {p}. p -> Expr -> Expr
ks }
    ks :: p -> Expr -> Expr
ks p
_ (F.PKVar KVar
k Subst
_) = KVar -> Subst -> Expr
F.PKVar KVar
k forall a. Monoid a => a
mempty
    ks p
_ Expr
p             = Expr
p

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

addPToEnv :: CGEnv
          -> PVar RSort -> CG CGEnv
addPToEnv :: CGEnv -> PVar (RType RTyCon RTyVar ()) -> CG CGEnv
addPToEnv CGEnv
γ PVar (RType RTyCon RTyVar ())
π
  = do CGEnv
γπ <- CGEnv
γ CGEnv -> ([Char], Symbol, SpecType) -> CG CGEnv
+= ([Char]
"addSpec1", forall t. PVar t -> Symbol
pname PVar (RType RTyCon RTyVar ())
π, forall r.
(PPrint r, Reftable r) =>
PVar (RType RTyCon RTyVar ()) -> RRType r
pvarRType PVar (RType RTyCon RTyVar ())
π)
       forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM CGEnv -> ([Char], Symbol, SpecType) -> CG CGEnv
(+=) CGEnv
γπ [([Char]
"addSpec2", Symbol
x, forall r c tv. Reftable r => RType c tv () -> RType c tv r
ofRSort RType RTyCon RTyVar ()
t) | (RType RTyCon RTyVar ()
t, Symbol
x, Expr
_) <- forall t. PVar t -> [(t, Symbol, Expr)]
pargs PVar (RType RTyCon RTyVar ())
π]

--------------------------------------------------------------------------------
-- | Bidirectional Constraint Generation: CHECKING -----------------------------
--------------------------------------------------------------------------------
cconsE :: CGEnv -> CoreExpr -> SpecType -> CG ()
--------------------------------------------------------------------------------
cconsE :: CGEnv -> CoreExpr -> SpecType -> StateT CGInfo Identity ()
cconsE CGEnv
g CoreExpr
e SpecType
t = do
  -- NOTE: tracing goes here
  -- traceM $ printf "cconsE:\n  expr = %s\n  exprType = %s\n  lqType = %s\n" (showPpr e) (showPpr (exprType e)) (showpp t)
  CGEnv -> CoreExpr -> SpecType -> StateT CGInfo Identity ()
cconsE' CGEnv
g CoreExpr
e SpecType
t

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

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

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

cconsE' CGEnv
γ CoreExpr
e (RAllP PVar (RType RTyCon RTyVar ())
p SpecType
t)
  = CGEnv -> CoreExpr -> SpecType -> StateT CGInfo Identity ()
cconsE CGEnv
γ' CoreExpr
e SpecType
t''
  where
    t' :: SpecType
t'         = (UsedPVar, (Symbol, [((), Symbol, Expr)]) -> Expr)
-> RReft -> RReft
replacePredsWithRefs forall {a} {b}. (UsedPVar, (Symbol, [(a, b, Expr)]) -> Expr)
su forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SpecType
t
    su :: (UsedPVar, (Symbol, [(a, b, Expr)]) -> Expr)
su         = (forall t. PVar t -> UsedPVar
uPVar PVar (RType RTyCon RTyVar ())
p, forall t a b. PVar t -> (Symbol, [(a, b, Expr)]) -> Expr
pVartoRConc PVar (RType RTyCon RTyVar ())
p)
    ([[(Symbol, SpecType)]]
css, SpecType
t'') = forall c tv r.
TyConable c =>
Bool -> RType c tv r -> ([[(Symbol, RType c tv r)]], RType c tv r)
splitConstraints (Config -> Bool
typeclass (forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)) SpecType
t'
    γ' :: CGEnv
γ'         = 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 CoreBind
b CoreExpr
e) SpecType
t
  = do CGEnv
γ' <- CGEnv -> CoreBind -> CG CGEnv
consCBLet CGEnv
γ CoreBind
b
       CGEnv -> CoreExpr -> SpecType -> StateT CGInfo Identity ()
cconsE CGEnv
γ' CoreExpr
e SpecType
t

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

cconsE' CGEnv
γ (Lam Id
α CoreExpr
e) (RAllT RTVar RTyVar (RType RTyCon RTyVar ())
α' SpecType
t RReft
r) | Id -> Bool
isTyVar Id
α
  = do CGEnv
γ' <- CGEnv -> Id -> CG CGEnv
updateEnvironment CGEnv
γ Id
α
       CGEnv -> Id -> CoreExpr -> SpecType -> StateT CGInfo Identity ()
addForAllConstraint CGEnv
γ' Id
α CoreExpr
e (forall c tv r. RTVU c tv -> RType c tv r -> r -> RType c tv r
RAllT RTVar RTyVar (RType RTyCon RTyVar ())
α' SpecType
t RReft
r)
       CGEnv -> CoreExpr -> SpecType -> StateT CGInfo Identity ()
cconsE CGEnv
γ' CoreExpr
e forall a b. (a -> b) -> a -> b
$ forall tv r c.
(Eq tv, Hashable tv, Reftable r, TyConable c,
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv,
 SubsTy tv (RType c tv ()) tv,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) =>
(tv, RType c tv r) -> RType c tv r -> RType c tv r
subsTyVarMeet' (forall tv s. RTVar tv s -> tv
ty_var_value RTVar RTyVar (RType RTyCon RTyVar ())
α', forall r c. Monoid r => Id -> RType c RTyVar r
rVar Id
α) SpecType
t

cconsE' CGEnv
γ (Lam Id
x CoreExpr
e) (RFun Symbol
y RFInfo
i SpecType
ty SpecType
t RReft
r)
  | Bool -> Bool
not (Id -> Bool
isTyVar Id
x)
  = do CGEnv
γ' <- CGEnv
γ CGEnv -> ([Char], Symbol, SpecType) -> CG CGEnv
+= ([Char]
"cconsE", Symbol
x', SpecType
ty)
       CGEnv -> CoreExpr -> SpecType -> StateT CGInfo Identity ()
cconsE CGEnv
γ' CoreExpr
e SpecType
t'
       CGEnv -> Id -> CoreExpr -> SpecType -> StateT CGInfo Identity ()
addFunctionConstraint CGEnv
γ Id
x CoreExpr
e (forall c tv r.
Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
x' RFInfo
i SpecType
ty SpecType
t' RReft
r')
       Id -> Annot SpecType -> StateT CGInfo Identity ()
addIdA Id
x (forall t. t -> Annot t
AnnDef SpecType
ty)
  where
    x' :: Symbol
x'  = forall a. Symbolic a => a -> Symbol
F.symbol Id
x
    t' :: SpecType
t'  = SpecType
t forall a. Subable a => a -> (Symbol, Expr) -> a
`F.subst1` (Symbol
y, Symbol -> Expr
F.EVar Symbol
x')
    r' :: RReft
r'  = RReft
r forall a. Subable a => a -> (Symbol, Expr) -> a
`F.subst1` (Symbol
y, Symbol -> Expr
F.EVar Symbol
x')

cconsE' CGEnv
γ (Tick CoreTickish
tt CoreExpr
e) SpecType
t
  = CGEnv -> CoreExpr -> SpecType -> StateT CGInfo Identity ()
cconsE (CGEnv
γ CGEnv -> Span -> CGEnv
`setLocation` CoreTickish -> Span
Sp.Tick CoreTickish
tt) CoreExpr
e SpecType
t

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

cconsE' CGEnv
γ e :: CoreExpr
e@(Cast CoreExpr
e' CoercionR
c) SpecType
t
  = do SpecType
t' <- CGEnv -> Type -> CoreExpr -> CoercionR -> CG SpecType
castTy CGEnv
γ (CoreExpr -> Type
exprType CoreExpr
e) CoreExpr
e' CoercionR
c
       SubC -> [Char] -> StateT CGInfo Identity ()
addC (CGEnv -> SpecType -> SpecType -> SubC
SubC CGEnv
γ (forall a. PPrint a => [Char] -> a -> a
F.notracepp ([Char]
"Casted Type for " forall a. [a] -> [a] -> [a]
++ forall a. Outputable a => a -> [Char]
GM.showPpr CoreExpr
e forall a. [a] -> [a] -> [a]
++ [Char]
"\n init type " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
showpp SpecType
t) SpecType
t') SpecType
t) ([Char]
"cconsE Cast: " forall a. [a] -> [a] -> [a]
++ forall a. Outputable a => a -> [Char]
GM.showPpr CoreExpr
e)

cconsE' CGEnv
γ CoreExpr
e SpecType
t
  = do SpecType
te  <- CGEnv -> CoreExpr -> CG SpecType
consE CGEnv
γ CoreExpr
e
       SpecType
te' <- CGEnv -> CoreExpr -> SpecType -> CG SpecType
instantiatePreds CGEnv
γ CoreExpr
e SpecType
te forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= CGEnv -> SpecType -> CG SpecType
addPost CGEnv
γ
       SubC -> [Char] -> StateT CGInfo Identity ()
addC (CGEnv -> SpecType -> SpecType -> SubC
SubC CGEnv
γ SpecType
te' SpecType
t) ([Char]
"cconsE: " forall a. [a] -> [a] -> [a]
++ [Char]
"\n t = " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
showpp SpecType
t forall a. [a] -> [a] -> [a]
++ [Char]
"\n te = " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
showpp SpecType
te forall a. [a] -> [a] -> [a]
++ forall a. Outputable a => a -> [Char]
GM.showPpr CoreExpr
e)

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

addForAllConstraint :: CGEnv -> Var -> CoreExpr -> SpecType -> CG ()
addForAllConstraint :: CGEnv -> Id -> CoreExpr -> SpecType -> StateT CGInfo Identity ()
addForAllConstraint CGEnv
γ Id
_ CoreExpr
_ (RAllT RTVar RTyVar (RType RTyCon RTyVar ())
rtv SpecType
rt RReft
rr)
  | forall r. Reftable r => r -> Bool
F.isTauto RReft
rr
  = forall (m :: * -> *) a. Monad m => a -> m a
return ()
  | Bool
otherwise
  = do SpecType
t'       <- forall (m :: * -> *) a. Freshable m a => Bool -> a -> m a
true (Config -> Bool
typeclass (forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)) SpecType
rt
       let truet :: RReft -> SpecType
truet = forall c tv r. RTVU c tv -> RType c tv r -> r -> RType c tv r
RAllT RTVar RTyVar (RType RTyCon RTyVar ())
rtv forall a b. (a -> b) -> a -> b
$ forall {c} {tv} {r}. RType c tv r -> RType c tv r
unRAllP SpecType
t'
       SubC -> [Char] -> StateT CGInfo Identity ()
addC (CGEnv -> SpecType -> SpecType -> SubC
SubC CGEnv
γ (RReft -> SpecType
truet forall a. Monoid a => a
mempty) forall a b. (a -> b) -> a -> b
$ RReft -> SpecType
truet RReft
rr) [Char]
"forall constraint true"
  where unRAllP :: RType c tv r -> RType c tv r
unRAllP (RAllT RTVU c tv
a RType c tv r
t r
r) = forall c tv r. RTVU c tv -> RType c tv r -> r -> RType c tv r
RAllT RTVU c tv
a (RType c tv r -> RType c tv r
unRAllP RType c tv r
t) r
r
        unRAllP (RAllP PVU c tv
_ RType c tv r
t)   = RType c tv r -> RType c tv r
unRAllP RType c tv r
t
        unRAllP RType c tv r
t             = RType c tv r
t
addForAllConstraint CGEnv
γ Id
_ CoreExpr
_ SpecType
_
  = forall a. Maybe SrcSpan -> [Char] -> a
impossible (forall a. a -> Maybe a
Just 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 -> Id -> CoreExpr -> SpecType -> StateT CGInfo Identity ()
addFunctionConstraint CGEnv
γ Id
x CoreExpr
e (RFun Symbol
y RFInfo
i SpecType
ty SpecType
t RReft
r)
  = do SpecType
ty'      <- forall (m :: * -> *) a. Freshable m a => Bool -> a -> m a
true (Config -> Bool
typeclass (forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)) SpecType
ty
       SpecType
t'       <- forall (m :: * -> *) a. Freshable m a => Bool -> a -> m a
true (Config -> Bool
typeclass (forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)) SpecType
t
       let truet :: RReft -> SpecType
truet = forall c tv r.
Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
y RFInfo
i SpecType
ty' SpecType
t'
       Maybe Expr
lamE <- CGEnv -> CoreExpr -> CG (Maybe Expr)
lamExpr CGEnv
γ CoreExpr
e
       case (Maybe Expr
lamE, forall t. HasConfig t => t -> Bool
higherOrderFlag CGEnv
γ) of
          (Just Expr
e', Bool
True) -> do TCEmb TyCon
tce    <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CGInfo -> TCEmb TyCon
tyConEmbed
                                let sx :: Sort
sx  = TCEmb TyCon -> Type -> Sort
typeSort TCEmb TyCon
tce forall a b. (a -> b) -> a -> b
$ Id -> Type
varType Id
x
                                let ref :: RReft
ref = forall r. r -> UReft r
uTop forall a b. (a -> b) -> a -> b
$ forall a. Expression a => a -> Reft
F.exprReft forall a b. (a -> b) -> a -> b
$ (Symbol, Sort) -> Expr -> Expr
F.ELam (forall a. Symbolic a => a -> Symbol
F.symbol Id
x, Sort
sx) Expr
e'
                                SubC -> [Char] -> StateT CGInfo Identity ()
addC (CGEnv -> SpecType -> SpecType -> SubC
SubC CGEnv
γ (RReft -> SpecType
truet RReft
ref) forall a b. (a -> b) -> a -> b
$ RReft -> SpecType
truet RReft
r) [Char]
"function constraint singleton"
          (Maybe Expr, Bool)
_ -> SubC -> [Char] -> StateT CGInfo Identity ()
addC (CGEnv -> SpecType -> SpecType -> SubC
SubC CGEnv
γ (RReft -> SpecType
truet forall a. Monoid a => a
mempty) forall a b. (a -> b) -> a -> b
$ RReft -> SpecType
truet RReft
r) [Char]
"function constraint true"
addFunctionConstraint CGEnv
γ Id
_ CoreExpr
_ SpecType
_
  = forall a. Maybe SrcSpan -> [Char] -> a
impossible (forall a. a -> Maybe a
Just 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, RType c tv r)]
cs r
_ Oblig
OCons RType c tv r
t)
  = let ([[(Symbol, RType c tv r)]]
css, RType c tv r
t') = forall c tv r.
TyConable c =>
Bool -> RType c tv r -> ([[(Symbol, RType c tv r)]], RType c tv r)
splitConstraints Bool
allowTC RType c tv r
t in ([(Symbol, RType c tv r)]
csforall a. a -> [a] -> [a]
:[[(Symbol, RType c tv r)]]
css, RType c tv r
t')
splitConstraints Bool
allowTC (RFun Symbol
x RFInfo
i tx :: RType c tv r
tx@(RApp c
c [RType c tv r]
_ [RTProp c tv r]
_ r
_) RType c tv r
t r
r) | forall {c}. TyConable c => c -> Bool
isErasable c
c
  = let ([[(Symbol, RType c tv r)]]
css, RType c tv r
t') = forall c tv r.
TyConable c =>
Bool -> RType c tv r -> ([[(Symbol, RType c tv r)]], RType c tv r)
splitConstraints Bool
allowTC  RType c tv r
t in ([[(Symbol, RType c tv r)]]
css, forall c tv r.
Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
x RFInfo
i RType c tv r
tx RType c tv r
t' r
r)
  where isErasable :: c -> Bool
isErasable = if Bool
allowTC then forall {c}. TyConable c => c -> Bool
isEmbeddedDict else forall {c}. TyConable c => c -> Bool
isClass
splitConstraints Bool
_ RType c tv r
t
  = ([], RType 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 -> CoreExpr -> SpecType -> CG SpecType
instantiatePreds CGEnv
γ CoreExpr
e (RAllP PVar (RType RTyCon RTyVar ())
π SpecType
t)
  = do RTProp RTyCon RTyVar RReft
r <- CGEnv
-> CoreExpr
-> PVar (RType RTyCon RTyVar ())
-> CG (RTProp RTyCon RTyVar RReft)
freshPredRef CGEnv
γ CoreExpr
e PVar (RType RTyCon RTyVar ())
π
       CGEnv -> CoreExpr -> SpecType -> CG SpecType
instantiatePreds CGEnv
γ CoreExpr
e forall a b. (a -> b) -> a -> b
$ [Char]
-> SpecType
-> [(PVar (RType RTyCon RTyVar ()), RTProp RTyCon RTyVar RReft)]
-> SpecType
replacePreds [Char]
"consE" SpecType
t [(PVar (RType RTyCon RTyVar ())
π, RTProp RTyCon RTyVar RReft
r)]

instantiatePreds CGEnv
_ CoreExpr
_ SpecType
t0
  = forall (m :: * -> *) a. Monad m => a -> m a
return SpecType
t0


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

--------------------------------------------------------------------------------
-- | Bidirectional Constraint Generation: SYNTHESIS ----------------------------
--------------------------------------------------------------------------------
consE :: CGEnv -> CoreExpr -> CG SpecType
--------------------------------------------------------------------------------
consE :: CGEnv -> CoreExpr -> CG SpecType
consE CGEnv
γ CoreExpr
e
  | forall t. HasConfig t => t -> Bool
patternFlag CGEnv
γ
  , Just Pattern
p <- CoreExpr -> Maybe Pattern
Rs.lift CoreExpr
e
  = CGEnv -> Pattern -> Type -> CG SpecType
consPattern CGEnv
γ (forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"CONSE-PATTERN: " Pattern
p) (CoreExpr -> Type
exprType CoreExpr
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 Id
x) | Id -> Bool
GM.isDataConId Id
x
  = do SpecType
t0 <- (?callStack::CallStack) => CGEnv -> Id -> CG SpecType
varRefType CGEnv
γ Id
x
       -- NV: The check is expected to fail most times, so
       --     it is cheaper than direclty fmap ignoreSelf.
       let hasSelf :: Bool
hasSelf = Symbol
selfSymbol forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` forall a. Subable a => a -> [Symbol]
F.syms SpecType
t0
       let t :: SpecType
t = if Bool
hasSelf
                then forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Reft -> Reft
ignoreSelf forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SpecType
t0
                else SpecType
t0
       Maybe Id -> SrcSpan -> Annot SpecType -> StateT CGInfo Identity ()
addLocA (forall a. a -> Maybe a
Just Id
x) (CGEnv -> SrcSpan
getLocation CGEnv
γ) (forall t. CGEnv -> Id -> t -> Annot t
varAnn CGEnv
γ Id
x SpecType
t)
       forall (m :: * -> *) a. Monad m => a -> m a
return SpecType
t

consE CGEnv
γ (Var Id
x)
  = do SpecType
t <- (?callStack::CallStack) => CGEnv -> Id -> CG SpecType
varRefType CGEnv
γ Id
x
       Maybe Id -> SrcSpan -> Annot SpecType -> StateT CGInfo Identity ()
addLocA (forall a. a -> Maybe a
Just Id
x) (CGEnv -> SrcSpan
getLocation CGEnv
γ) (forall t. CGEnv -> Id -> t -> Annot t
varAnn CGEnv
γ Id
x SpecType
t)
       forall (m :: * -> *) a. Monad m => a -> m a
return SpecType
t

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

consE CGEnv
γ e' :: CoreExpr
e'@(App CoreExpr
e a :: CoreExpr
a@(Type Type
τ))
  = do RAllT RTVar RTyVar (RType RTyCon RTyVar ())
α SpecType
te RReft
_ <- forall a.
Outputable a =>
([Char], a) -> CGEnv -> SpecType -> SpecType
checkAll ([Char]
"Non-all TyApp with expr", CoreExpr
e) CGEnv
γ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CGEnv -> CoreExpr -> CG SpecType
consE CGEnv
γ CoreExpr
e
       SpecType
t            <- if Bool -> Bool
not (Config -> Bool
nopolyinfer (forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)) Bool -> Bool -> Bool
&& forall {tv} {s}. RTVar tv s -> Bool
isPos RTVar RTyVar (RType RTyCon RTyVar ())
α Bool -> Bool -> Bool
&& RTyVar -> SpecType -> Bool
isGenericVar (forall tv s. RTVar tv s -> tv
ty_var_value RTVar RTyVar (RType RTyCon RTyVar ())
α) SpecType
te
                         then Bool -> KVKind -> CoreExpr -> Type -> CG SpecType
freshTyType (Config -> Bool
typeclass (forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)) KVKind
TypeInstE CoreExpr
e Type
τ
                         else Bool -> Type -> CG SpecType
trueTy (Config -> Bool
typeclass (forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)) Type
τ
       WfC -> StateT CGInfo Identity ()
addW          forall a b. (a -> b) -> a -> b
$ CGEnv -> SpecType -> WfC
WfC CGEnv
γ SpecType
t
       SpecType
t'           <- forall (m :: * -> *). FreshM m => SpecType -> m SpecType
refreshVV SpecType
t
       SpecType
tt0          <- CGEnv -> CoreExpr -> SpecType -> CG SpecType
instantiatePreds CGEnv
γ CoreExpr
e' (forall tv r c.
(Eq tv, Hashable tv, Reftable r, TyConable c,
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv,
 SubsTy tv (RType c tv ()) tv,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) =>
(tv, RType c tv r) -> RType c tv r -> RType c tv r
subsTyVarMeet' (forall tv s. RTVar tv s -> tv
ty_var_value RTVar RTyVar (RType RTyCon RTyVar ())
α, SpecType
t') SpecType
te)
       let tt :: SpecType
tt        = CGEnv -> CoreExpr -> SpecType -> SpecType
makeSingleton CGEnv
γ (CoreExpr -> CoreExpr
simplify CoreExpr
e') forall a b. (a -> b) -> a -> b
$ CGEnv -> RTyVar -> Type -> SpecType -> SpecType
subsTyReft CGEnv
γ (forall tv s. RTVar tv s -> tv
ty_var_value RTVar RTyVar (RType RTyCon RTyVar ())
α) Type
τ SpecType
tt0
       forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ case forall s. RTVar RTyVar s -> Maybe (Symbol, s)
rTVarToBind RTVar RTyVar (RType RTyCon RTyVar ())
α of
         Just (Symbol
x, RType RTyCon RTyVar ()
_) -> forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall a a2.
(Show a, Show a2, Subable a) =>
CGEnv -> CoreExpr -> Symbol -> a -> a2 -> a
checkUnbound CGEnv
γ CoreExpr
e' Symbol
x SpecType
tt CoreExpr
a) (forall a. Subable a => a -> (Symbol, Expr) -> a
F.subst1 SpecType
tt forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol
x,)) (Type -> Maybe Expr
argType Type
τ)
         Maybe (Symbol, RType RTyCon RTyVar ())
Nothing     -> SpecType
tt
  where
    isPos :: RTVar tv s -> Bool
isPos RTVar tv s
α = Bool -> Bool
not (Config -> Bool
extensionality (forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)) Bool -> Bool -> Bool
|| forall s. RTVInfo s -> Bool
rtv_is_pol (forall tv s. RTVar tv s -> RTVInfo s
ty_var_info RTVar tv s
α)

consE CGEnv
γ e' :: CoreExpr
e'@(App CoreExpr
e CoreExpr
a) | Just Id
aDict <- CGEnv -> CoreExpr -> Maybe Id
getExprDict CGEnv
γ CoreExpr
a
  = case forall a1 a.
(Symbolic a1, Show a) =>
Maybe (HashMap Symbol a) -> a1 -> Maybe a
dhasinfo (forall k t.
(Eq k, Hashable k) =>
DEnv k t -> k -> Maybe (HashMap Symbol (RISig t))
dlookup (CGEnv -> RDEnv
denv CGEnv
γ) Id
aDict) (CGEnv -> CoreExpr -> Id
getExprFun CGEnv
γ CoreExpr
e) of
      Just RISig SpecType
riSig -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. RISig a -> a
fromRISig RISig SpecType
riSig
      Maybe (RISig SpecType)
_          -> do
        ([], [PVar (RType RTyCon RTyVar ())]
πs, SpecType
te) <- forall tv c r.
RType tv c r
-> ([(RTVar c (RType tv c ()), r)], [PVar (RType tv c ())],
    RType tv c r)
bkUniv forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CGEnv -> CoreExpr -> CG SpecType
consE CGEnv
γ CoreExpr
e
        SpecType
te'          <- CGEnv -> CoreExpr -> SpecType -> CG SpecType
instantiatePreds CGEnv
γ CoreExpr
e' forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall c tv r. PVU c tv -> RType c tv r -> RType c tv r
RAllP SpecType
te [PVar (RType RTyCon RTyVar ())]
πs
        (CGEnv
γ', SpecType
te''')  <- CGEnv -> SpecType -> CG (CGEnv, SpecType)
dropExists CGEnv
γ SpecType
te'
        SpecType
te''         <- CGEnv -> SpecType -> CG SpecType
dropConstraints CGEnv
γ SpecType
te'''
        Maybe SrcSpan -> SpecType -> StateT CGInfo Identity ()
updateLocA {- πs -} (CoreExpr -> Maybe SrcSpan
exprLoc CoreExpr
e) SpecType
te''
        let RFun Symbol
x RFInfo
_ SpecType
tx SpecType
t RReft
_ = forall a.
Outputable a =>
([Char], a) -> CGEnv -> SpecType -> SpecType
checkFun ([Char]
"Non-fun App with caller ", CoreExpr
e') CGEnv
γ SpecType
te''
        CGEnv -> CoreExpr -> SpecType -> StateT CGInfo Identity ()
cconsE CGEnv
γ' CoreExpr
a SpecType
tx
        CGEnv -> SpecType -> CG SpecType
addPost CGEnv
γ'        forall a b. (a -> b) -> a -> b
$ forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall a a2.
(Show a, Show a2, Subable a) =>
CGEnv -> CoreExpr -> Symbol -> a -> a2 -> a
checkUnbound CGEnv
γ' CoreExpr
e' Symbol
x SpecType
t CoreExpr
a) (forall a. Subable a => a -> (Symbol, Expr) -> a
F.subst1 SpecType
t forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol
x,)) (CGEnv -> CoreExpr -> Maybe Expr
argExpr CGEnv
γ CoreExpr
a)

consE CGEnv
γ e' :: CoreExpr
e'@(App CoreExpr
e CoreExpr
a)
  = do ([], [PVar (RType RTyCon RTyVar ())]
πs, SpecType
te) <- forall tv c r.
RType tv c r
-> ([(RTVar c (RType tv c ()), r)], [PVar (RType tv c ())],
    RType tv c r)
bkUniv forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CGEnv -> CoreExpr -> CG SpecType
consE CGEnv
γ {- GM.tracePpr ("APP-EXPR: " ++ GM.showPpr (exprType e)) -} CoreExpr
e
       SpecType
te1        <- CGEnv -> CoreExpr -> SpecType -> CG SpecType
instantiatePreds CGEnv
γ CoreExpr
e' forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall c tv r. PVU c tv -> RType c tv r -> RType c tv r
RAllP SpecType
te [PVar (RType RTyCon RTyVar ())]
πs
       (CGEnv
γ', SpecType
te2)  <- CGEnv -> SpecType -> CG (CGEnv, SpecType)
dropExists CGEnv
γ SpecType
te1
       SpecType
te3        <- CGEnv -> SpecType -> CG SpecType
dropConstraints CGEnv
γ SpecType
te2
       Maybe SrcSpan -> SpecType -> StateT CGInfo Identity ()
updateLocA (CoreExpr -> Maybe SrcSpan
exprLoc CoreExpr
e) SpecType
te3
       let RFun Symbol
x RFInfo
_ SpecType
tx SpecType
t RReft
_ = forall a.
Outputable a =>
([Char], a) -> CGEnv -> SpecType -> SpecType
checkFun ([Char]
"Non-fun App with caller ", CoreExpr
e') CGEnv
γ SpecType
te3
       CGEnv -> CoreExpr -> SpecType -> StateT CGInfo Identity ()
cconsE CGEnv
γ' CoreExpr
a SpecType
tx
       CGEnv -> CoreExpr -> SpecType -> SpecType
makeSingleton CGEnv
γ' (CoreExpr -> CoreExpr
simplify CoreExpr
e') forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CGEnv -> SpecType -> CG SpecType
addPost CGEnv
γ' (forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall a a2.
(Show a, Show a2, Subable a) =>
CGEnv -> CoreExpr -> Symbol -> a -> a2 -> a
checkUnbound CGEnv
γ' CoreExpr
e' Symbol
x SpecType
t CoreExpr
a) (forall a. Subable a => a -> (Symbol, Expr) -> a
F.subst1 SpecType
t forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol
x,)) (CGEnv -> CoreExpr -> Maybe Expr
argExpr CGEnv
γ forall a b. (a -> b) -> a -> b
$ CoreExpr -> CoreExpr
simplify CoreExpr
a))

consE CGEnv
γ (Lam Id
α CoreExpr
e) | Id -> Bool
isTyVar Id
α
  = do CGEnv
γ' <- CGEnv -> Id -> CG CGEnv
updateEnvironment CGEnv
γ Id
α
       SpecType
t' <- CGEnv -> CoreExpr -> CG SpecType
consE CGEnv
γ' CoreExpr
e
       forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall c tv r. RTVU c tv -> RType c tv r -> r -> RType c tv r
RAllT (forall tv s. tv -> RTVar tv s
makeRTVar forall a b. (a -> b) -> a -> b
$ Id -> RTyVar
rTyVar Id
α) SpecType
t' forall a. Monoid a => a
mempty

consE CGEnv
γ  e :: CoreExpr
e@(Lam Id
x CoreExpr
e1)
  = do SpecType
tx      <- Bool -> KVKind -> CoreExpr -> Type -> CG SpecType
freshTyType (Config -> Bool
typeclass (forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)) KVKind
LamE (forall b. Id -> Expr b
Var Id
x) Type
τx
       CGEnv
γ'      <- CGEnv
γ CGEnv -> ([Char], Symbol, SpecType) -> CG CGEnv
+= ([Char]
"consE", forall a. Symbolic a => a -> Symbol
F.symbol Id
x, SpecType
tx)
       SpecType
t1      <- CGEnv -> CoreExpr -> CG SpecType
consE CGEnv
γ' CoreExpr
e1
       Id -> Annot SpecType -> StateT CGInfo Identity ()
addIdA Id
x forall a b. (a -> b) -> a -> b
$ forall t. t -> Annot t
AnnDef SpecType
tx
       WfC -> StateT CGInfo Identity ()
addW     forall a b. (a -> b) -> a -> b
$ CGEnv -> SpecType -> WfC
WfC CGEnv
γ SpecType
tx
       TCEmb TyCon
tce     <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CGInfo -> TCEmb TyCon
tyConEmbed
       RReft
lamSing <- CGEnv -> TCEmb TyCon -> Id -> CoreExpr -> CG RReft
lambdaSingleton CGEnv
γ TCEmb TyCon
tce Id
x CoreExpr
e1
       forall (m :: * -> *) a. Monad m => a -> m a
return   forall a b. (a -> b) -> a -> b
$ forall c tv r.
Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun (forall a. Symbolic a => a -> Symbol
F.symbol Id
x) (Config -> RFInfo
mkRFInfo forall a b. (a -> b) -> a -> b
$ forall t. HasConfig t => t -> Config
getConfig CGEnv
γ) SpecType
tx SpecType
t1 RReft
lamSing
    where
      FunTy { ft_arg :: Type -> Type
ft_arg = Type
τx } = CoreExpr -> Type
exprType CoreExpr
e

consE CGEnv
γ e :: CoreExpr
e@(Let CoreBind
_ CoreExpr
_)
  = KVKind -> CGEnv -> CoreExpr -> CG SpecType
cconsFreshE KVKind
LetE CGEnv
γ CoreExpr
e

consE CGEnv
γ e :: CoreExpr
e@(Case CoreExpr
_ Id
_ Type
_ [Alt Id
_])
  | Just p :: Pattern
p@Rs.PatProject{} <- CoreExpr -> Maybe Pattern
Rs.lift CoreExpr
e
  = CGEnv -> Pattern -> Type -> CG SpecType
consPattern CGEnv
γ Pattern
p (CoreExpr -> Type
exprType CoreExpr
e)

consE CGEnv
γ e :: CoreExpr
e@(Case CoreExpr
_ Id
_ Type
_ [Alt Id]
cs)
  = KVKind -> CGEnv -> CoreExpr -> CG SpecType
cconsFreshE ([Alt Id] -> KVKind
caseKVKind [Alt Id]
cs) CGEnv
γ CoreExpr
e

consE CGEnv
γ (Tick CoreTickish
tt CoreExpr
e)
  = do SpecType
t <- CGEnv -> CoreExpr -> CG SpecType
consE (CGEnv -> Span -> CGEnv
setLocation CGEnv
γ (CoreTickish -> Span
Sp.Tick CoreTickish
tt)) CoreExpr
e
       Maybe Id -> SrcSpan -> Annot SpecType -> StateT CGInfo Identity ()
addLocA forall a. Maybe a
Nothing (CoreTickish -> SrcSpan
GM.tickSrcSpan CoreTickish
tt) (forall t. t -> Annot t
AnnUse SpecType
t)
       forall (m :: * -> *) a. Monad m => a -> m a
return SpecType
t

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

consE CGEnv
γ e :: CoreExpr
e@(Cast CoreExpr
e' CoercionR
c)
  = CGEnv -> Type -> CoreExpr -> CoercionR -> CG SpecType
castTy CGEnv
γ (CoreExpr -> Type
exprType CoreExpr
e) CoreExpr
e' CoercionR
c

consE CGEnv
γ e :: CoreExpr
e@(Coercion CoercionR
_)
   = Bool -> Type -> CG SpecType
trueTy (Config -> Bool
typeclass (forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)) forall a b. (a -> b) -> a -> b
$ CoreExpr -> Type
exprType CoreExpr
e

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

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

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

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

-- | `exprDict e` returns the dictionary `Var` inside the expression `e`
getExprDict :: CGEnv -> CoreExpr -> Maybe Var
getExprDict :: CGEnv -> CoreExpr -> Maybe Id
getExprDict CGEnv
γ           =  forall {b}. Expr b -> Maybe Id
go
  where
    go :: Expr b -> Maybe Id
go (Var Id
x)          = case forall k t.
(Eq k, Hashable k) =>
DEnv k t -> k -> Maybe (HashMap Symbol (RISig t))
dlookup (CGEnv -> RDEnv
denv CGEnv
γ) Id
x of {Just HashMap Symbol (RISig SpecType)
_ -> forall a. a -> Maybe a
Just Id
x; Maybe (HashMap Symbol (RISig SpecType))
Nothing -> forall a. Maybe a
Nothing}
    go (Tick CoreTickish
_ Expr b
e)       = Expr b -> Maybe Id
go Expr b
e
    go (App Expr b
a (Type Type
_)) = Expr b -> Maybe Id
go Expr b
a
    go (Let Bind b
_ Expr b
e)        = Expr b -> Maybe Id
go Expr b
e
    go Expr b
_                = 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 = forall c tv.
(Symbol -> Expr -> Expr) -> RType c tv RReft -> RType c tv RReft
mapExprReft (\Symbol
_ -> CoSub -> Expr -> Expr
F.applyCoSub CoSub
coSub)
  where
    coSub :: CoSub
coSub        = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [(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 -> CG SpecType
consPattern CGEnv
γ (Rs.PatBind CoreExpr
e1 Id
x CoreExpr
e2 Type
_ CoreExpr
_ Type
_ Type
_ Id
_) Type
_ = do
  SpecType
tx <- forall a.
Outputable a =>
([Char], a) -> CGEnv -> SpecType -> SpecType
checkMonad (forall {a}. IsString a => a
msg, CoreExpr
e1) CGEnv
γ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CGEnv -> CoreExpr -> CG SpecType
consE CGEnv
γ CoreExpr
e1
  CGEnv
γ' <- CGEnv
γ CGEnv -> ([Char], Symbol, SpecType) -> CG CGEnv
+= ([Char]
"consPattern", forall a. Symbolic a => a -> Symbol
F.symbol Id
x, SpecType
tx)
  Id -> Annot SpecType -> StateT CGInfo Identity ()
addIdA Id
x (forall t. t -> Annot t
AnnDef SpecType
tx)
  CGEnv -> CoreExpr -> CG SpecType
consE CGEnv
γ' CoreExpr
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 CoreExpr
e Type
m CoreExpr
_ Type
_ Id
_) Type
t = do
  SpecType
et    <- forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"Cons-Pattern-Ret" forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CGEnv -> CoreExpr -> CG SpecType
consE CGEnv
γ CoreExpr
e
  SpecType
mt    <- Bool -> Type -> CG SpecType
trueTy (Config -> Bool
typeclass (forall t. HasConfig t => t -> Config
getConfig CGEnv
γ))  Type
m
  SpecType
tt    <- Bool -> Type -> CG SpecType
trueTy (Config -> Bool
typeclass (forall t. HasConfig t => t -> Config
getConfig CGEnv
γ))  Type
t
  forall (m :: * -> *) a. Monad m => a -> m a
return (SpecType -> SpecType -> SpecType -> SpecType
mkRAppTy SpecType
mt SpecType
et SpecType
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 Id
xe Id
_ Type
τ DataCon
c [Id]
ys Int
i) Type
_ = do
  let yi :: Id
yi = [Id]
ys forall a. [a] -> Int -> a
!! Int
i
  SpecType
t    <- (WfC -> StateT CGInfo Identity ()
addW forall b c a. (b -> c) -> (a -> b) -> a -> c
. CGEnv -> SpecType -> WfC
WfC CGEnv
γ) forall (m :: * -> *) b a. Monad m => (b -> m a) -> m b -> m b
<<= Bool -> KVKind -> CoreExpr -> Type -> CG SpecType
freshTyType (Config -> Bool
typeclass (forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)) KVKind
ProjectE (forall b. Id -> Expr b
Var Id
yi) Type
τ
  CGEnv
γ'   <- CGEnv
-> Id -> [AltCon] -> AltCon -> [Id] -> Maybe [Int] -> CG CGEnv
caseEnv CGEnv
γ Id
xe [] (DataCon -> AltCon
DataAlt DataCon
c) [Id]
ys (forall a. a -> Maybe a
Just [Int
i])
  SpecType
ti   <- {- γ' ??= yi -} (?callStack::CallStack) => CGEnv -> Id -> CG SpecType
varRefType CGEnv
γ' Id
yi
  SubC -> [Char] -> StateT CGInfo Identity ()
addC (CGEnv -> SpecType -> SpecType -> SubC
SubC CGEnv
γ' SpecType
ti SpecType
t) [Char]
"consPattern:project"
  forall (m :: * -> *) a. Monad m => a -> m a
return SpecType
t

consPattern CGEnv
γ (Rs.PatSelfBind Id
_ CoreExpr
e) Type
_ =
  CGEnv -> CoreExpr -> CG SpecType
consE CGEnv
γ CoreExpr
e

consPattern CGEnv
γ p :: Pattern
p@Rs.PatSelfRecBind{} Type
_ =
  KVKind -> CGEnv -> CoreExpr -> CG SpecType
cconsFreshE KVKind
LetE CGEnv
γ (Pattern -> CoreExpr
Rs.lower Pattern
p)

mkRAppTy :: SpecType -> SpecType -> SpecType -> SpecType
mkRAppTy :: SpecType -> SpecType -> SpecType -> SpecType
mkRAppTy SpecType
mt SpecType
et RAppTy{}          = forall c tv r. RType c tv r -> RType c tv r -> r -> RType c tv r
RAppTy SpecType
mt SpecType
et forall a. Monoid a => a
mempty
mkRAppTy SpecType
_  SpecType
et (RApp RTyCon
c [SpecType
_] [] RReft
_) = forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp RTyCon
c [SpecType
et] [] forall a. Monoid a => a
mempty
mkRAppTy SpecType
_  SpecType
_  SpecType
_                 = forall a. Maybe SrcSpan -> [Char] -> a
panic 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 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 (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SpecType]
ts) = forall a. [a] -> a
last [SpecType]
ts
   go (RAppTy SpecType
_ SpecType
t RReft
_) = SpecType
t
   go SpecType
t              = 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 -> CoreExpr -> CoercionR -> CG SpecType
castTy CGEnv
γ Type
t CoreExpr
e (AxiomInstCo CoAxiom Branched
ca Int
_ [CoercionR]
_)
  = forall a. a -> Maybe a -> a
fromMaybe forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CGEnv -> Type -> CoreExpr -> CG SpecType
castTy' CGEnv
γ Type
t CoreExpr
e forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TyCon -> CG (Maybe SpecType)
lookupNewType (forall (br :: BranchFlag). CoAxiom br -> TyCon
coAxiomTyCon CoAxiom Branched
ca)

castTy CGEnv
γ Type
t CoreExpr
e (SymCo (AxiomInstCo CoAxiom Branched
ca Int
_ [CoercionR]
_))
  = do Maybe SpecType
mtc <- TyCon -> CG (Maybe SpecType)
lookupNewType (forall (br :: BranchFlag). CoAxiom br -> TyCon
coAxiomTyCon CoAxiom Branched
ca)
       forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
F.forM_ Maybe SpecType
mtc (CGEnv -> CoreExpr -> SpecType -> StateT CGInfo Identity ()
cconsE CGEnv
γ CoreExpr
e)
       CGEnv -> Type -> CoreExpr -> CG SpecType
castTy' CGEnv
γ Type
t CoreExpr
e

castTy CGEnv
γ Type
t CoreExpr
e CoercionR
_
  = CGEnv -> Type -> CoreExpr -> CG SpecType
castTy' CGEnv
γ Type
t CoreExpr
e


castTy' :: CGEnv -> Type -> CoreExpr -> CG SpecType
castTy' CGEnv
γ Type
τ (Var Id
x)
  = do SpecType
t0 <- Bool -> Type -> CG SpecType
trueTy (Config -> Bool
typeclass (forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)) Type
τ
       SpecType
tx <- (?callStack::CallStack) => CGEnv -> Id -> CG SpecType
varRefType CGEnv
γ Id
x
       let t :: SpecType
t = SpecType -> SpecType -> SpecType
mergeCastTys SpecType
t0 SpecType
tx
       let ce :: Expr
ce = if Config -> Bool
typeclass (forall t. HasConfig t => t -> Config
getConfig CGEnv
γ) Bool -> Bool -> Bool
&& Config -> Bool
noADT (forall t. HasConfig t => t -> Config
getConfig CGEnv
γ) then forall a. Expression a => a -> Expr
F.expr Id
x
                  else Sort -> Sort -> Expr -> Expr
eCoerc (TCEmb TyCon -> Type -> Sort
typeSort (CGEnv -> TCEmb TyCon
emb CGEnv
γ) forall a b. (a -> b) -> a -> b
$ Type -> Type
Ghc.expandTypeSynonyms forall a b. (a -> b) -> a -> b
$ Id -> Type
varType Id
x)
                         (TCEmb TyCon -> Type -> Sort
typeSort (CGEnv -> TCEmb TyCon
emb CGEnv
γ) Type
τ)
                         forall a b. (a -> b) -> a -> b
$ forall a. Expression a => a -> Expr
F.expr Id
x
       forall (m :: * -> *) a. Monad m => a -> m a
return (SpecType
t forall r c tv. Reftable r => RType c tv r -> r -> RType c tv r
`strengthen` forall r. r -> UReft r
uTop (forall a. Expression a => a -> Reft
F.uexprReft Expr
ce) {- `F.meet` tx -})
  where eCoerc :: Sort -> Sort -> Expr -> Expr
eCoerc Sort
s Sort
t Expr
e
         | Sort
s forall a. Eq a => a -> a -> Bool
== Sort
t    = Expr
e
         | Bool
otherwise = Sort -> Sort -> Expr -> Expr
F.ECoerc Sort
s Sort
t Expr
e

castTy' CGEnv
γ Type
t (Tick CoreTickish
_ CoreExpr
e)
  = CGEnv -> Type -> CoreExpr -> CG SpecType
castTy' CGEnv
γ Type
t CoreExpr
e

castTy' CGEnv
_ Type
_ CoreExpr
e
  = forall a. Maybe SrcSpan -> [Char] -> a
panic forall a. Maybe a
Nothing forall a b. (a -> b) -> a -> b
$ [Char]
"castTy cannot handle expr " forall a. [a] -> [a] -> [a]
++ forall a. Outputable a => a -> [Char]
GM.showPpr CoreExpr
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
  | forall r. ToTypeable r => Bool -> RRType r -> Type
toType Bool
False SpecType
t1 forall a. Eq a => a -> a -> Bool
== 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 forall a. Eq a => a -> a -> Bool
== RTyCon
c2
  = forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp RTyCon
c1 (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 (CoreExpr -> CoreExpr)
isClassConCo CoercionR
co
  | Pair Type
t1 Type
t2 <- 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]    <- forall a b. (a -> b) -> [a] -> [b]
map 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 (forall a. Uniquable a => [a] -> UniqSet a
mkUniqSet forall a b. (a -> b) -> a -> b
$ TyCon -> [Id]
tyConTyVars TyCon
tc) (InScopeSet -> RnEnv2
mkRnEnv2 InScopeSet
emptyInScopeSet) TvSubstEnv
emptyTvSubstEnv Type
tm Type
t1
  = forall a. a -> Maybe a
Just (\CoreExpr
e -> DataCon -> [CoreExpr] -> CoreExpr
mkCoreConApps DataCon
dc forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall b. Type -> Expr b
Type [Type]
ts forall a. [a] -> [a] -> [a]
++ [CoreExpr
e])

  | Bool
otherwise
  = 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 -> CoreExpr -> CG SpecType
cconsFreshE KVKind
kvkind CGEnv
γ CoreExpr
e = do
  SpecType
t   <- Bool -> KVKind -> CoreExpr -> Type -> CG SpecType
freshTyType (Config -> Bool
typeclass (forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)) KVKind
kvkind CoreExpr
e forall a b. (a -> b) -> a -> b
$ CoreExpr -> Type
exprType CoreExpr
e
  WfC -> StateT CGInfo Identity ()
addW forall a b. (a -> b) -> a -> b
$ CGEnv -> SpecType -> WfC
WfC CGEnv
γ SpecType
t
  CGEnv -> CoreExpr -> SpecType -> StateT CGInfo Identity ()
cconsE CGEnv
γ CoreExpr
e SpecType
t
  forall (m :: * -> *) a. Monad m => a -> m a
return SpecType
t
--------------------------------------------------------------------------------

checkUnbound :: (Show a, Show a2, F.Subable a)
             => CGEnv -> CoreExpr -> F.Symbol -> a -> a2 -> a
checkUnbound :: forall a a2.
(Show a, Show a2, Subable a) =>
CGEnv -> CoreExpr -> Symbol -> a -> a2 -> a
checkUnbound CGEnv
γ CoreExpr
e Symbol
x a
t a2
a
  | Symbol
x forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` forall a. Subable a => a -> [Symbol]
F.syms a
t = a
t
  | Bool
otherwise            = forall a. Maybe SrcSpan -> [Char] -> a
panic (forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ CGEnv -> SrcSpan
getLocation CGEnv
γ) [Char]
msg
  where
    msg :: [Char]
msg = [[Char]] -> [Char]
unlines [ [Char]
"checkUnbound: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Symbol
x forall a. [a] -> [a] -> [a]
++ [Char]
" is elem of syms of " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show a
t
                  , [Char]
"In"
                  , forall a. Outputable a => a -> [Char]
GM.showPpr CoreExpr
e
                  , [Char]
"Arg = "
                  , 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) 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            = forall (m :: * -> *) a. Monad m => a -> m a
return (CGEnv
γ, SpecType
t)

dropConstraints :: CGEnv -> SpecType -> CG SpecType
dropConstraints :: CGEnv -> SpecType -> CG 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) | forall {c}. TyConable c => c -> Bool
isErasable RTyCon
c
  = forall a b c. (a -> b -> c) -> b -> a -> c
flip (forall c tv r.
Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
x RFInfo
i SpecType
tx) RReft
r forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CGEnv -> SpecType -> CG SpecType
dropConstraints CGEnv
cgenv SpecType
t
  where
    isErasable :: c -> Bool
isErasable = if Config -> Bool
typeclass (forall t. HasConfig t => t -> Config
getConfig CGEnv
cgenv) then forall {c}. TyConable c => c -> Bool
isEmbeddedDict else forall {c}. TyConable c => c -> Bool
isClass
dropConstraints CGEnv
cgenv (RRTy [(Symbol, SpecType)]
cts RReft
_ Oblig
OCons SpecType
rt)
  = do 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
       SubC -> [Char] -> StateT CGInfo Identity ()
addC (CGEnv -> SpecType -> SpecType -> SubC
SubC CGEnv
γ' SpecType
t1 SpecType
t2)  [Char]
"dropConstraints"
       CGEnv -> SpecType -> CG SpecType
dropConstraints CGEnv
cgenv SpecType
rt
  where
    ([(Symbol, SpecType)]
xts, SpecType
t1, SpecType
t2) = forall a b. [(a, b)] -> ([(a, b)], b, b)
envToSub [(Symbol, SpecType)]
cts

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

-------------------------------------------------------------------------------------
cconsCase :: CGEnv -> Var -> SpecType -> [AltCon] -> CoreAlt -> CG ()
-------------------------------------------------------------------------------------
cconsCase :: CGEnv
-> Id
-> SpecType
-> [AltCon]
-> Alt Id
-> StateT CGInfo Identity ()
cconsCase CGEnv
γ Id
x SpecType
t [AltCon]
acs (Alt AltCon
ac [Id]
ys CoreExpr
ce)
  = do CGEnv
cγ <- CGEnv
-> Id -> [AltCon] -> AltCon -> [Id] -> Maybe [Int] -> CG CGEnv
caseEnv CGEnv
γ Id
x [AltCon]
acs AltCon
ac [Id]
ys forall a. Monoid a => a
mempty
       CGEnv -> CoreExpr -> SpecType -> StateT CGInfo Identity ()
cconsE CGEnv
cγ CoreExpr
ce SpecType
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
-> Id -> [AltCon] -> AltCon -> [Id] -> Maybe [Int] -> CG CGEnv
caseEnv CGEnv
γ Id
x [AltCon]
_   (DataAlt DataCon
c) [Id]
ys Maybe [Int]
pIs = do

  let (Symbol
x' : [Symbol]
ys')   = forall a. Symbolic a => a -> Symbol
F.symbol forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Id
xforall a. a -> [a] -> [a]
:[Id]
ys)
  SpecType
xt0             <- forall a.
Outputable a =>
([Char], a) -> CGEnv -> SpecType -> SpecType
checkTyCon ([Char]
"checkTycon cconsCase", Id
x) CGEnv
γ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CGEnv
γ (?callStack::CallStack) => CGEnv -> Id -> CG SpecType
??= Id
x
  let rt :: SpecType
rt           = forall c (f :: * -> *) tv.
(TyConable c, Reftable (f Reft), Functor f) =>
RType c tv (f Reft) -> Symbol -> RType c tv (f Reft)
shiftVV SpecType
xt0 Symbol
x'
  SpecType
tdc             <- CGEnv
γ (?callStack::CallStack) => CGEnv -> Id -> CG SpecType
??= DataCon -> Id
dataConWorkId DataCon
c forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (m :: * -> *). FreshM m => SpecType -> m SpecType
refreshVV
  let (SpecType
rtd,[SpecType]
yts',SpecType
_) = SpecType -> SpecType -> [Id] -> (SpecType, [SpecType], SpecType)
unfoldR SpecType
tdc SpecType
rt [Id]
ys
  [SpecType]
yts             <- Bool -> Maybe [Int] -> [SpecType] -> CG [SpecType]
projectTypes (Config -> Bool
typeclass (forall t. HasConfig t => t -> Config
getConfig CGEnv
γ))  Maybe [Int]
pIs [SpecType]
yts'
  let ys'' :: [Symbol]
ys''         = forall a. Symbolic a => a -> Symbol
F.symbol forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. if Bool
allowTC then Id -> Bool
GM.isEmbeddedDictVar else Id -> Bool
GM.isEvVar) [Id]
ys
  let r1 :: Reft
r1           = DataCon -> [Symbol] -> Reft
dataConReft   DataCon
c   [Symbol]
ys''
  let r2 :: Reft
r2           = forall r c tv. Reftable r => RType c tv r -> [Symbol] -> Reft
dataConMsReft SpecType
rtd [Symbol]
ys''
  let xt :: SpecType
xt           = (SpecType
xt0 forall r. Reftable r => r -> r -> r
`F.meet` SpecType
rtd) forall r c tv. Reftable r => RType c tv r -> r -> RType c tv r
`strengthen` forall r. r -> UReft r
uTop (Reft
r1 forall r. Reftable r => r -> r -> r
`F.meet` Reft
r2)
  let cbs :: [(Symbol, SpecType)]
cbs          = forall a b.
(?callStack::CallStack) =>
[Char] -> [a] -> [b] -> [(a, b)]
safeZip [Char]
"cconsCase" (Symbol
x'forall a. a -> [a] -> [a]
:[Symbol]
ys')
                         (forall a b. (a -> b) -> [a] -> [b]
map (forall a. Subable a => a -> (Symbol, Expr) -> a
`F.subst1` (Symbol
selfSymbol, Symbol -> Expr
F.EVar Symbol
x'))
                         (SpecType
xt0 forall a. a -> [a] -> [a]
: [SpecType]
yts))
  CGEnv
cγ'             <- CGEnv -> Symbol -> [(Symbol, SpecType)] -> CG CGEnv
addBinders CGEnv
γ Symbol
x' [(Symbol, SpecType)]
cbs
  CGEnv -> Symbol -> [(Symbol, SpecType)] -> CG CGEnv
addBinders CGEnv
cγ' Symbol
x' [(Symbol
x', RReft -> RReft
substSelf forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SpecType
xt)]
  where allowTC :: Bool
allowTC    = Config -> Bool
typeclass (forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)

caseEnv CGEnv
γ Id
x [AltCon]
acs AltCon
a [Id]
_ Maybe [Int]
_ = do
  let x' :: Symbol
x'  = forall a. Symbolic a => a -> Symbol
F.symbol Id
x
  SpecType
xt'    <- (forall r c tv. Reftable r => RType c tv r -> r -> RType c tv r
`strengthen` forall r. r -> UReft r
uTop (CGEnv -> [AltCon] -> AltCon -> Reft
altReft CGEnv
γ [AltCon]
acs AltCon
a)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (CGEnv
γ (?callStack::CallStack) => CGEnv -> Id -> CG SpecType
??= Id
x)
  CGEnv -> Symbol -> [(Symbol, SpecType)] -> CG CGEnv
addBinders CGEnv
γ Symbol
x' [(Symbol
x', SpecType
xt')]


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

substSelf :: UReft F.Reft -> UReft F.Reft
substSelf :: RReft -> RReft
substSelf (MkUReft Reft
r Predicate
p) = forall r. r -> Predicate -> UReft r
MkUReft (Reft -> Reft
substSelfReft Reft
r) Predicate
p

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

ignoreSelf :: F.Reft -> F.Reft
ignoreSelf :: Reft -> Reft
ignoreSelf = forall t. Visitable t => (Expr -> Expr) -> t -> t
F.mapExpr (\Expr
r -> if Symbol
selfSymbol forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` forall a. Subable a => a -> [Symbol]
F.syms Expr
r then Expr
F.PTrue else Expr
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] -> CG [SpecType]
projectTypes Bool
_        Maybe [Int]
Nothing    [SpecType]
ts = forall (m :: * -> *) a. Monad m => a -> m a
return [SpecType]
ts
projectTypes Bool
allowTC (Just [Int]
ints) [SpecType]
ts = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall {t :: * -> *} {a} {m :: * -> *} {a}.
(Foldable t, Eq a, Freshable m a) =>
t a -> (a, a) -> m a
projT [Int]
ints) (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 forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t a
is = forall (m :: * -> *) a. Monad m => a -> m a
return a
t
      | Bool
otherwise   = 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 -> Reft
altReft CGEnv
_ [AltCon]
_   (LitAlt Literal
l) = Literal -> Reft
literalFReft Literal
l
altReft CGEnv
γ [AltCon]
acs AltCon
DEFAULT    = forall a. Monoid a => [a] -> a
mconcat ([Literal -> Reft
notLiteralReft Literal
l | LitAlt Literal
l <- [AltCon]
acs] forall a. [a] -> [a] -> [a]
++ [DataCon -> Reft
notDataConReft DataCon
d | DataAlt DataCon
d <- [AltCon]
acs])
  where
    notLiteralReft :: Literal -> Reft
notLiteralReft   = forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. Monoid a => a
mempty forall a. Expression a => a -> Reft
F.notExprReft forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCEmb TyCon -> Literal -> (Sort, Maybe Expr)
literalConst (CGEnv -> TCEmb TyCon
emb CGEnv
γ)
    notDataConReft :: DataCon -> Reft
notDataConReft DataCon
d | Config -> Bool
exactDC (forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)
                     = (Symbol, Expr) -> Reft
F.Reft (Symbol
F.vv_, Expr -> Expr
F.PNot (Expr -> Expr -> Expr
F.EApp (Symbol -> Expr
F.EVar forall a b. (a -> b) -> a -> b
$ DataCon -> Symbol
makeDataConChecker DataCon
d) (Symbol -> Expr
F.EVar Symbol
F.vv_)))
                     | Bool
otherwise = forall a. Monoid a => a
mempty
altReft CGEnv
_ [AltCon]
_ AltCon
_            = forall a. Maybe SrcSpan -> [Char] -> a
panic forall a. Maybe a
Nothing [Char]
"Constraint : altReft"

unfoldR :: SpecType -> SpecType -> [Var] -> (SpecType, [SpecType], SpecType)
unfoldR :: SpecType -> SpecType -> [Id] -> (SpecType, [SpecType], SpecType)
unfoldR SpecType
td (RApp RTyCon
_ [SpecType]
ts [RTProp RTyCon RTyVar RReft]
rs RReft
_) [Id]
ys = (SpecType
t3, forall {r}. Monoid r => [RRType r]
tvys forall a. [a] -> [a] -> [a]
++ [SpecType]
yts, forall {c} {tv} {r}. RType c tv r -> RType 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) (forall a. [a] -> [a]
reverse [RTProp RTyCon RTyVar RReft]
rs)
        (([Symbol]
ys0,[RFInfo]
_,[SpecType]
yts',[RReft]
_), SpecType
rt) = 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 (forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
msg forall a b. (a -> b) -> a -> b
$ SpecType -> [SpecType] -> SpecType
instantiateTys SpecType
tbody [SpecType]
tvs')
        msg :: [Char]
msg                  = [Char]
"INST-TY: " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
F.showpp (SpecType
td, [SpecType]
ts, SpecType
tbody, [Id]
ys, [SpecType]
tvs')
        yts'' :: [SpecType]
yts''                = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall a. Subable a => Subst -> a -> a
F.subst [Subst]
sus ([SpecType]
yts'forall a. [a] -> [a] -> [a]
++[SpecType
rt])
        (SpecType
t3,[SpecType]
yts)             = (forall a. [a] -> a
last [SpecType]
yts'', forall a. [a] -> [a]
init [SpecType]
yts'')
        sus :: [Subst]
sus                  = [(Symbol, Expr)] -> Subst
F.mkSubst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. [a] -> [[a]]
L.inits [(Symbol
x, Symbol -> Expr
F.EVar Symbol
y) | (Symbol
x, Symbol
y) <- forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
ys0 [Symbol]
ys']
        ([Id]
αs, [Symbol]
ys')            = forall b c a. (b -> c) -> (a, b) -> (a, c)
mapSnd (forall a. Symbolic a => a -> Symbol
F.symbol forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> ([a], [a])
L.partition Id -> Bool
isTyVar [Id]
ys
        tvs' :: [SpecType]
        tvs' :: [SpecType]
tvs'                 = forall r c. Monoid r => Id -> RType c RTyVar r
rVar forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Id]
αs
        tvys :: [RRType r]
tvys                 = forall r. Monoid r => Type -> RRType r
ofType forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Type
varType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Id]
αs

unfoldR SpecType
_  SpecType
_                [Id]
_  = forall a. Maybe SrcSpan -> [Char] -> a
panic forall a. Maybe a
Nothing [Char]
"Constraint.hs : unfoldR"

instantiateTys :: SpecType -> [SpecType] -> SpecType
instantiateTys :: SpecType -> [SpecType] -> SpecType
instantiateTys = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' forall {tv} {r} {c}.
(Hashable tv, Reftable r, TyConable c, FreeVar c tv,
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) tv,
 SubsTy tv (RType c tv ()) (RType c tv ()),
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) =>
RType c tv r -> RType c tv r -> RType c tv r
go
  where
    go :: RType c tv r -> RType c tv r -> RType c tv r
go (RAllT RTVar tv (RType c tv ())
α RType c tv r
tbody r
_) RType c tv r
t = forall tv r c.
(Eq tv, Hashable tv, Reftable r, TyConable c,
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv,
 SubsTy tv (RType c tv ()) tv,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) =>
(tv, RType c tv r) -> RType c tv r -> RType c tv r
subsTyVarMeet' (forall tv s. RTVar tv s -> tv
ty_var_value RTVar tv (RType c tv ())
α, RType c tv r
t) RType c tv r
tbody
    go RType c tv r
_ RType c tv r
_                 = forall a. Maybe SrcSpan -> [Char] -> a
panic forall a. Maybe a
Nothing [Char]
"Constraint.instantiateTy"

instantiatePvs :: SpecType -> [SpecProp] -> SpecType
instantiatePvs :: SpecType -> [RTProp RTyCon RTyVar RReft] -> SpecType
instantiatePvs           = 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 PVar (RType RTyCon RTyVar ())
p SpecType
tbody) RTProp RTyCon RTyVar RReft
r = [Char]
-> SpecType
-> [(PVar (RType RTyCon RTyVar ()), RTProp RTyCon RTyVar RReft)]
-> SpecType
replacePreds [Char]
"instantiatePv" SpecType
tbody [(PVar (RType RTyCon RTyVar ())
p, RTProp RTyCon RTyVar RReft
r)]
    go SpecType
t               RTProp RTyCon RTyVar RReft
_ = forall a. [Char] -> [Char] -> a
errorP [Char]
"" ([Char]
"Constraint.instantiatePvs: t = " forall a. [a] -> [a] -> [a]
++ 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        = 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        = 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         = 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 = forall a. Maybe SrcSpan -> [Char] -> a
panic (forall a. a -> Maybe a
Just SrcSpan
sp) forall a b. (a -> b) -> a -> b
$ [Char]
msg forall a. [a] -> [a] -> [a]
++ forall a. Outputable a => a -> [Char]
GM.showPpr a
e forall a. [a] -> [a] -> [a]
++ [Char]
", type: " forall a. [a] -> [a] -> [a]
++ 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 -> Id -> t -> Annot t
varAnn CGEnv
γ Id
x t
t
  | Id
x forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`S.member` CGEnv -> HashSet Id
recs CGEnv
γ = forall t. SrcSpan -> Annot t
AnnLoc (forall a. NamedThing a => a -> SrcSpan
getSrcSpan Id
x)
  | Bool
otherwise           = forall t. t -> Annot t
AnnUse t
t

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

freshPredRef CGEnv
_ CoreExpr
_ (PV Symbol
_ PVKind (RType RTyCon RTyVar ())
PVHProp Symbol
_ [(RType RTyCon RTyVar (), Symbol, Expr)]
_)
  = forall a. Maybe SrcSpan -> [Char] -> a
todo forall a. Maybe a
Nothing [Char]
"EFFECTS:freshPredRef"


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


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


lamExpr :: CGEnv -> CoreExpr -> CG (Maybe F.Expr)
lamExpr :: CGEnv -> CoreExpr -> CG (Maybe Expr)
lamExpr CGEnv
g CoreExpr
e = do
    [DataDecl]
adts <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CGInfo -> [DataDecl]
cgADTs
    Bool
allowTC <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CGInfo -> Bool
cgiTypeclass
    let dm :: DataConMap
dm = [DataDecl] -> DataConMap
dataConMap [DataDecl]
adts
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. Either a b -> Maybe b
eitherToMaybe forall a b. (a -> b) -> a -> b
$ forall t.
TCEmb TyCon
-> LogicMap
-> DataConMap
-> ([Char] -> TError SpecType)
-> LogicM t
-> Either (TError SpecType) t
runToLogic (CGEnv -> TCEmb TyCon
emb CGEnv
g) forall a. Monoid a => a
mempty DataConMap
dm
      (\[Char]
x -> forall a. Maybe SrcSpan -> [Char] -> a
todo forall a. Maybe a
Nothing ([Char]
"coreToLogic not working lamExpr: " forall a. [a] -> [a] -> [a]
++ [Char]
x))
      (Bool -> CoreExpr -> LogicM Expr
coreToLogic Bool
allowTC CoreExpr
e)

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


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

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

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



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

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

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

funExpr CGEnv
_ CoreExpr
_
  = forall a. Maybe a
Nothing

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


singletonReft :: (F.Symbolic a) => a -> UReft F.Reft
singletonReft :: forall a. Symbolic a => a -> RReft
singletonReft = forall r. r -> UReft r
uTop forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Symbolic a => a -> Reft
F.symbolReft forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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, F.Reftable r) => RType c tv r -> r -> RType c tv r
strengthenTop :: forall {r} {c} {tv}.
(PPrint r, Reftable r) =>
RType c tv r -> r -> RType c tv r
strengthenTop (RApp c
c [RType c tv r]
ts [RTProp c tv r]
rs r
r) r
r'   = forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp c
c [RType c tv r]
ts [RTProp c tv r]
rs   forall a b. (a -> b) -> a -> b
$ forall r. Reftable r => r -> r -> r
F.meet r
r r
r'
strengthenTop (RVar tv
a r
r) r
r'         = forall c tv r. tv -> r -> RType c tv r
RVar tv
a         forall a b. (a -> b) -> a -> b
$ forall r. Reftable r => r -> r -> r
F.meet r
r r
r'
strengthenTop (RFun Symbol
b RFInfo
i RType c tv r
t1 RType c tv r
t2 r
r) r
r' = forall c tv r.
Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
b RFInfo
i RType c tv r
t1 RType c tv r
t2 forall a b. (a -> b) -> a -> b
$ forall r. Reftable r => r -> r -> r
F.meet r
r r
r'
strengthenTop (RAppTy RType c tv r
t1 RType c tv r
t2 r
r) r
r'   = forall c tv r. RType c tv r -> RType c tv r -> r -> RType c tv r
RAppTy RType c tv r
t1 RType c tv r
t2   forall a b. (a -> b) -> a -> b
$ forall r. Reftable r => r -> r -> r
F.meet r
r r
r'
strengthenTop (RAllT RTVU c tv
a RType c tv r
t r
r)    r
r'   = forall c tv r. RTVU c tv -> RType c tv r -> r -> RType c tv r
RAllT RTVU c tv
a RType c tv r
t      forall a b. (a -> b) -> a -> b
$ forall r. Reftable r => r -> r -> r
F.meet r
r r
r'
strengthenTop RType c tv r
t r
_                   = RType c tv r
t

-- TODO: this is almost identical to RT.strengthen! merge them!
strengthenMeet :: (PPrint r, F.Reftable r) => RType c tv r -> r -> RType c tv r
strengthenMeet :: forall {r} {c} {tv}.
(PPrint r, Reftable r) =>
RType c tv r -> r -> RType c tv r
strengthenMeet (RApp c
c [RType c tv r]
ts [RTProp c tv r]
rs r
r) r
r'  = forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp c
c [RType c tv r]
ts [RTProp c tv r]
rs (r
r forall r. Reftable r => r -> r -> r
`F.meet` r
r')
strengthenMeet (RVar tv
a r
r) r
r'        = forall c tv r. tv -> r -> RType c tv r
RVar tv
a       (r
r forall r. Reftable r => r -> r -> r
`F.meet` r
r')
strengthenMeet (RFun Symbol
b RFInfo
i RType c tv r
t1 RType c tv r
t2 r
r) r
r'= forall c tv r.
Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
b RFInfo
i RType c tv r
t1 RType c tv r
t2 (r
r forall r. Reftable r => r -> r -> r
`F.meet` r
r')
strengthenMeet (RAppTy RType c tv r
t1 RType c tv r
t2 r
r) r
r'  = forall c tv r. RType c tv r -> RType c tv r -> r -> RType c tv r
RAppTy RType c tv r
t1 RType c tv r
t2 (r
r forall r. Reftable r => r -> r -> r
`F.meet` r
r')
strengthenMeet (RAllT RTVU c tv
a RType c tv r
t r
r) r
r'     = forall c tv r. RTVU c tv -> RType c tv r -> r -> RType c tv r
RAllT RTVU c tv
a (forall {r} {c} {tv}.
(PPrint r, Reftable r) =>
RType c tv r -> r -> RType c tv r
strengthenMeet RType c tv r
t r
r') (r
r forall r. Reftable r => r -> r -> r
`F.meet` r
r')
strengthenMeet RType c tv r
t r
_                  = RType c tv r
t

-- topMeet :: (PPrint r, F.Reftable r) => r -> r -> r
-- topMeet r r' = r `F.meet` r'

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

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

-- | @isGenericVar@ determines whether the @RTyVar@ has no class constraints
isGenericVar :: RTyVar -> SpecType -> Bool
isGenericVar :: RTyVar -> SpecType -> Bool
isGenericVar RTyVar
α SpecType
st =  forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\(Class
c, RTyVar
α') -> (RTyVar
α'forall a. Eq a => a -> a -> Bool
/=RTyVar
α) Bool -> Bool -> Bool
|| Class -> Bool
isGenericClass Class
c ) (forall {b} {r}.
(PPrint b, PPrint r, Reftable r, Reftable (RTProp RTyCon b r),
 Reftable (RTProp RTyCon b ()), Hashable b) =>
RType RTyCon b r -> [(Class, b)]
classConstrs SpecType
st)
  where
    classConstrs :: RType RTyCon b r -> [(Class, b)]
classConstrs RType RTyCon b r
t = [(Class
c, forall tv s. RTVar tv s -> tv
ty_var_value RTVar b (RType RTyCon b ())
α')
                        | (Class
c, [RType RTyCon b r]
ts) <- forall tv r.
OkRT RTyCon tv r =>
RType RTyCon tv r -> [(Class, [RType RTyCon tv r])]
tyClasses RType RTyCon b r
t
                        , RType RTyCon b r
t'      <- [RType RTyCon b r]
ts
                        , RTVar b (RType RTyCon b ())
α'      <- forall tv c r. Eq tv => RType c tv r -> [RTVar tv (RType c tv ())]
freeTyVars RType RTyCon b r
t']
    isGenericClass :: Class -> Bool
isGenericClass Class
c = Class -> Name
className Class
c 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. [Char] -> Identity a
fail [Char]
msg = forall a. Maybe SrcSpan -> [Char] -> a
panic forall a. Maybe a
Nothing [Char]
msg