{-# 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 #-}
{-# OPTIONS_GHC -Wno-x-partial #-}

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

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

import           Prelude                                       hiding (error)
import           GHC.Stack ( CallStack )
import           Liquid.GHC.API               as Ghc hiding ( panic
                                                            , (<+>)
                                                            , text
                                                            , vcat
                                                            )
import qualified Language.Haskell.Liquid.GHC.Resugar           as Rs
import qualified Language.Haskell.Liquid.GHC.SpanStack         as Sp
import qualified Language.Haskell.Liquid.GHC.Misc              as GM -- ( isInternal, collectArguments, tickSrcSpan, showPpr )
import Text.PrettyPrint.HughesPJ ( text )
import           Control.Monad ( foldM, forM, forM_, when, void )
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, safeZip )
import           Language.Fixpoint.Types.Visitor
import qualified Language.Fixpoint.Types                       as F
import qualified Language.Fixpoint.Types.Visitor               as F
import           Language.Haskell.Liquid.Constraint.Fresh ( addKuts, freshTyType, trueTy )
import           Language.Haskell.Liquid.Constraint.Init ( initEnv, initCGI )
import           Language.Haskell.Liquid.Constraint.Env
import           Language.Haskell.Liquid.Constraint.Monad
import Language.Haskell.Liquid.Constraint.Split ( splitC, splitW )
import           Language.Haskell.Liquid.Constraint.Relational (consAssmRel, consRelTop)
import           Language.Haskell.Liquid.Types.Dictionaries
import           Language.Haskell.Liquid.Types.Errors
import           Language.Haskell.Liquid.Types.Fresh
import           Language.Haskell.Liquid.Types.Literals
import           Language.Haskell.Liquid.Types.Names
import           Language.Haskell.Liquid.Types.PredType
import           Language.Haskell.Liquid.Types.RType
import           Language.Haskell.Liquid.Types.RTypeOp
import           Language.Haskell.Liquid.Types.RefType
import           Language.Haskell.Liquid.Types.Specs
import           Language.Haskell.Liquid.Types.Types hiding (binds)
import           Language.Haskell.Liquid.Constraint.Types
import           Language.Haskell.Liquid.Constraint.Constraint ( addConstraints )
import           Language.Haskell.Liquid.Constraint.Template
import           Language.Haskell.Liquid.Constraint.Termination
import           Language.Haskell.Liquid.Constraint.RewriteCase
import           Language.Haskell.Liquid.Transforms.CoreToLogic (weakenResult, runToLogic, coreToLogic)
import           Language.Haskell.Liquid.Bare.DataType (dataConMap, makeDataConChecker)
import Language.Haskell.Liquid.UX.Config
    ( HasConfig(getConfig),
      Config(typeclass, gradual, checkDerived, extensionality,
             nopolyinfer, noADT, dependantCase, exactDC, rankNTypes),
      patternFlag,
      higherOrderFlag )

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

consAct :: CGEnv -> Config -> TargetInfo -> CG ()
consAct :: CGEnv -> Config -> TargetInfo -> State CGInfo ()
consAct CGEnv
γ Config
cfg TargetInfo
info = do
  let sSpc :: GhcSpecSig
sSpc = TargetSpec -> GhcSpecSig
gsSig (TargetSpec -> GhcSpecSig)
-> (TargetInfo -> TargetSpec) -> TargetInfo -> GhcSpecSig
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TargetInfo -> TargetSpec
giSpec (TargetInfo -> GhcSpecSig) -> TargetInfo -> GhcSpecSig
forall a b. (a -> b) -> a -> b
$ TargetInfo
info
  let gSrc :: TargetSrc
gSrc = TargetInfo -> TargetSrc
giSrc TargetInfo
info
  Bool -> State CGInfo () -> State CGInfo ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Config -> Bool
gradual Config
cfg) (((Id, Located SpecType) -> State CGInfo ())
-> [(Id, Located SpecType)] -> State CGInfo ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (WfC -> State CGInfo ()
addW (WfC -> State CGInfo ())
-> ((Id, Located SpecType) -> WfC)
-> (Id, Located SpecType)
-> State CGInfo ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CGEnv -> SpecType -> WfC
WfC CGEnv
γ (SpecType -> WfC)
-> ((Id, Located SpecType) -> SpecType)
-> (Id, Located SpecType)
-> WfC
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located SpecType -> SpecType
forall a. Located a -> a
val (Located SpecType -> SpecType)
-> ((Id, Located SpecType) -> Located SpecType)
-> (Id, Located SpecType)
-> SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Id, Located SpecType) -> Located SpecType
forall a b. (a, b) -> b
snd) (GhcSpecSig -> [(Id, Located SpecType)]
gsTySigs GhcSpecSig
sSpc [(Id, Located SpecType)]
-> [(Id, Located SpecType)] -> [(Id, Located SpecType)]
forall a. [a] -> [a] -> [a]
++ GhcSpecSig -> [(Id, Located SpecType)]
gsAsmSigs GhcSpecSig
sSpc))
  γ' <- (CGEnv -> CoreBind -> CG CGEnv) -> CGEnv -> [CoreBind] -> CG 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
  (ψ, γ'') <- foldM (consAssmRel cfg info) ([], γ') (gsAsmRel sSpc ++ gsRelation sSpc)
  mapM_ (consRelTop cfg info γ'' ψ) (gsRelation sSpc)
  -- End: Relational Checking
  mapM_ (consClass γ) (gsMethods $ gsSig $ giSpec info)
  hcs <- gets hsCs
  hws <- gets hsWfs
  fcs <- concat <$> mapM (splitC (typeclass (getConfig info))) hcs
  fws <- concat <$> mapM splitW hws
  modify $ \CGInfo
st -> CGInfo
st { fEnv     = fEnv    st `mappend` feEnv (fenv γ)
                     , cgLits   = litEnv   γ
                     , cgConsts = cgConsts st `mappend` constEnv γ
                     , fixCs    = fcs
                     , fixWfs   = 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)) -> State CGInfo ()
consClass CGEnv
γ (Id
x,MethodType (Located SpecType)
mt)
  | Just Located SpecType
ti <- MethodType (Located SpecType) -> Maybe (Located SpecType)
forall t. MethodType t -> Maybe t
tyInstance MethodType (Located SpecType)
mt
  , Just Located SpecType
tc <- MethodType (Located SpecType) -> Maybe (Located SpecType)
forall t. MethodType t -> Maybe t
tyClass    MethodType (Located SpecType)
mt
  = SubC -> [Char] -> State CGInfo ()
addC (CGEnv -> SpecType -> SpecType -> SubC
SubC (CGEnv
γ CGEnv -> Span -> CGEnv
`setLocation` SrcSpan -> Span
Sp.Span (SourcePos -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan (Located SpecType -> SourcePos
forall a. Located a -> SourcePos
F.loc Located SpecType
ti))) (Located SpecType -> SpecType
forall a. Located a -> a
val Located SpecType
ti) (Located SpecType -> SpecType
forall a. Located a -> a
val Located SpecType
tc)) ([Char]
"cconsClass for " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Id -> [Char]
forall a. Outputable a => a -> [Char]
GM.showPpr Id
x)
consClass CGEnv
_ (Id, MethodType (Located SpecType))
_
  = () -> State CGInfo ()
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

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

--------------------------------------------------------------------------------
-- | Constraint Generation: Corebind -------------------------------------------
--------------------------------------------------------------------------------
consCBTop :: Config -> TargetInfo -> CGEnv -> CoreBind -> CG CGEnv
--------------------------------------------------------------------------------
consCBTop :: Config -> TargetInfo -> CGEnv -> CoreBind -> CG CGEnv
consCBTop Config
cfg TargetInfo
info CGEnv
cgenv CoreBind
cb
  | (Id -> Bool) -> [Id] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Id -> Bool
trustVar [Id]
xs
  = (CGEnv -> Id -> CG CGEnv) -> CGEnv -> [Id] -> CG CGEnv
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   = CoreBind -> [Id]
forall b. Bind b -> [b]
bindersOf CoreBind
cb
       tt :: Id -> CG SpecType
tt   = Bool -> Type -> CG SpecType
trueTy (Config -> Bool
typeclass Config
cfg) (Type -> CG SpecType) -> (Id -> Type) -> Id -> CG SpecType
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 CG SpecType -> (SpecType -> CG CGEnv) -> CG CGEnv
forall a b.
StateT CGInfo Identity a
-> (a -> StateT CGInfo Identity b) -> StateT CGInfo Identity b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (\SpecType
t -> CGEnv
γ CGEnv -> ([Char], Symbol, SpecType) -> CG CGEnv
+= ([Char]
"derived", Id -> Symbol
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 oldtcheck <- (CGInfo -> Bool) -> StateT CGInfo Identity Bool
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CGInfo -> Bool
tcheck
       -- lazyVars  <- specLazy <$> get
       isStr     <- doTermCheck (getConfig γ) cb
       modify $ \CGInfo
s -> CGInfo
s { tcheck = oldtcheck && isStr}
       -- remove invariants that came from the cb definition
       let (γ', i) = removeInvariant γ cb                 --- DIFF
       γ'' <- consCB (mkTCheck oldtcheck isStr) (γ'{cgVar = topBind cb}) cb
       modify $ \CGInfo
s -> CGInfo
s { tcheck = oldtcheck}
       return $ restoreInvariant γ'' i                    --- DIFF
    where
      topBind :: Bind a -> Maybe a
topBind (NonRec a
v Expr a
_)  = a -> Maybe a
forall a. a -> Maybe a
Just a
v
      topBind (Rec [(a
v,Expr a
_)]) = a -> Maybe a
forall a. a -> Maybe a
Just a
v
      topBind Bind a
_             = Maybe a
forall a. Maybe a
Nothing

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

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

-- | NV: Dictionaries are not checked, because
-- | class methods' preconditions are not satisfied
consCB TCheck
_ CGEnv
γ (NonRec Id
x CoreExpr
_) | Id -> Bool
isDictionary Id
x
  = do t  <- Bool -> Type -> CG SpecType
trueTy (Config -> Bool
typeclass (CGEnv -> Config
forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)) (Id -> Type
varType Id
x)
       extender γ (x, Assumed t)
    where
       isDictionary :: Id -> Bool
isDictionary = Maybe (HashMap Symbol (RISig SpecType)) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (HashMap Symbol (RISig SpecType)) -> Bool)
-> (Id -> Maybe (HashMap Symbol (RISig SpecType))) -> Id -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DEnv Id SpecType -> Id -> Maybe (HashMap Symbol (RISig SpecType))
forall k t.
(Eq k, Hashable k) =>
DEnv k t -> k -> Maybe (HashMap Symbol (RISig t))
dlookup (CGEnv -> DEnv Id SpecType
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      <- DEnv Id SpecType -> Id -> Maybe (HashMap Symbol (RISig SpecType))
forall k t.
(Eq k, Hashable k) =>
DEnv k t -> k -> Maybe (HashMap Symbol (RISig t))
dlookup (CGEnv -> DEnv Id SpecType
denv CGEnv
γ) Id
w
  = do st       <- (Type -> CG SpecType)
-> [Type] -> StateT CGInfo Identity [SpecType]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Bool -> Type -> CG SpecType
trueTy (Config -> Bool
typeclass (CGEnv -> Config
forall t. HasConfig t => t -> Config
getConfig CGEnv
γ))) [Type]
τ
       mapM_ addW (WfC γ <$> st)
       let xts   = (RISig SpecType -> RISig SpecType)
-> HashMap Symbol (RISig SpecType)
-> HashMap Symbol (RISig SpecType)
forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
dmap ((SpecType -> SpecType) -> RISig SpecType -> RISig SpecType
forall a b. (a -> b) -> RISig a -> RISig b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([SpecType] -> SpecType -> SpecType
forall {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
γ { denv = dinsert (denv γ) x xts }
       t        <- trueTy (typeclass (getConfig γ)) (varType x)
       extender γ' (x, Assumed 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
_) = (tv, RType c tv r) -> RType c tv r -> RType c tv 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' (RTVar tv (RType c tv ()) -> tv
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 (RType c tv r -> RType c tv r) -> RType c tv r -> RType c tv r
forall a b. (a -> b) -> a -> b
$ (tv, RType c tv r) -> RType c tv r -> RType c tv 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' (RTVar tv (RType c tv ()) -> tv
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
_ = Maybe SrcSpan -> [Char] -> RType c tv r
forall a. Maybe SrcSpan -> [Char] -> a
impossible Maybe SrcSpan
forall a. Maybe a
Nothing [Char]
"consCB on Dictionary: this should not happen"

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

grepDictionary :: CoreExpr -> Maybe (Var, [Type])
grepDictionary :: CoreExpr -> Maybe (Id, [Type])
grepDictionary = [Type] -> CoreExpr -> Maybe (Id, [Type])
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)) = (Id, [Type]) -> Maybe (Id, [Type])
forall a. a -> Maybe a
Just (Id
w, [Type] -> [Type]
forall a. [a] -> [a]
reverse (Type
tType -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:[Type]
ts))
    go [Type]
ts (App Expr b
e (Type Type
t))       = [Type] -> Expr b -> Maybe (Id, [Type])
go (Type
tType -> [Type] -> [Type]
forall 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
_                       = Maybe (Id, [Type])
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
  = Template SpecType -> CG (Template SpecType)
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Template SpecType -> CG (Template SpecType))
-> Template SpecType -> CG (Template SpecType)
forall a b. (a -> b) -> a -> b
$ [Char] -> Template SpecType -> Template SpecType
forall a. PPrint a => [Char] -> a -> a
F.notracepp ([Char]
"TYPE FOR SELECTOR " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Id -> [Char]
forall a. Show a => a -> [Char]
show Id
x) (Template SpecType -> Template SpecType)
-> Template SpecType -> Template SpecType
forall a b. (a -> b) -> a -> b
$ SpecType -> Template SpecType
forall a. a -> Template a
Assumed SpecType
t

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

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

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

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

killSubst :: RReft -> RReft
killSubst :: RReft -> RReft
killSubst = (Reft -> Reft) -> RReft -> RReft
forall a b. (a -> b) -> UReftV Symbol a -> UReftV Symbol b
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 = (ExprV Symbol -> ExprV Symbol) -> Reft -> Reft
forall t. Visitable t => (ExprV Symbol -> ExprV Symbol) -> t -> t
trans ExprV Symbol -> ExprV Symbol
forall {v}. Monoid (SubstV v) => ExprV v -> ExprV v
ks
  where
    ks :: ExprV v -> ExprV v
ks (F.PKVar KVar
k SubstV v
_) = KVar -> SubstV v -> ExprV v
forall v. KVar -> SubstV v -> ExprV v
F.PKVar KVar
k SubstV v
forall a. Monoid a => a
mempty
    ks ExprV v
p             = ExprV v
p

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

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

--------------------------------------------------------------------------------
-- | Bidirectional Constraint Generation: CHECKING -----------------------------
--------------------------------------------------------------------------------
cconsE :: CGEnv -> CoreExpr -> SpecType -> CG ()
--------------------------------------------------------------------------------
cconsE :: CGEnv -> CoreExpr -> SpecType -> State CGInfo ()
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 -> State CGInfo ()
cconsE' CGEnv
g CoreExpr
e SpecType
t

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

  | Just (Rs.PatSelfRecBind Id
x CoreExpr
e') <- CoreExpr -> Maybe Pattern
Rs.lift CoreExpr
e
  = let γ' :: CGEnv
γ' = CGEnv
γ { grtys = insertREnv (F.symbol x) t (grtys γ)}
    in CG CGEnv -> State CGInfo ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (CG CGEnv -> State CGInfo ()) -> CG CGEnv -> State CGInfo ()
forall a b. (a -> b) -> a -> b
$ CGEnv -> CoreBind -> CG CGEnv
consCBLet CGEnv
γ' ([(Id, CoreExpr)] -> CoreBind
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 sp <- (CGInfo -> HashSet Id) -> StateT CGInfo Identity (HashSet Id)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CGInfo -> HashSet Id
specLVars
       if x `S.member` sp
         then cconsLazyLet γ e t
         else do γ' <- consCBLet γ b
                 cconsE γ' ee t

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

cconsE' CGEnv
γ (Let CoreBind
b CoreExpr
e) SpecType
t
  = do γ' <- CGEnv -> CoreBind -> CG CGEnv
consCBLet CGEnv
γ CoreBind
b
       cconsE γ' e t

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

cconsE' CGEnv
γ (Lam Id
α CoreExpr
e) (RAllT RTVar RTyVar (RType RTyCon RTyVar ())
α' SpecType
t RReft
r) | Id -> Bool
isTyVar Id
α
  = do γ' <- CGEnv -> Id -> CG CGEnv
updateEnvironment CGEnv
γ Id
α
       addForAllConstraint γ' α e (RAllT α' t r)
       cconsE γ' e $ subsTyVarMeet' (ty_var_value α', rVar α) 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 -> ([Char], Symbol, SpecType) -> CG CGEnv
+= ([Char]
"cconsE", Symbol
x', SpecType
ty)
       cconsE γ' e t'
       addFunctionConstraint γ x e (RFun x' i ty t' r')
       addIdA x (AnnDef ty)
  where
    x' :: Symbol
x'  = Id -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Id
x
    t' :: SpecType
t'  = SpecType
t SpecType -> (Symbol, ExprV Symbol) -> SpecType
forall a. Subable a => a -> (Symbol, ExprV Symbol) -> a
`F.subst1` (Symbol
y, Symbol -> ExprV Symbol
forall v. v -> ExprV v
F.EVar Symbol
x')
    r' :: RReft
r'  = RReft
r RReft -> (Symbol, ExprV Symbol) -> RReft
forall a. Subable a => a -> (Symbol, ExprV Symbol) -> a
`F.subst1` (Symbol
y, Symbol -> ExprV Symbol
forall v. v -> ExprV v
F.EVar Symbol
x')

cconsE' CGEnv
γ (Tick CoreTickish
tt CoreExpr
e) SpecType
t
  = CGEnv -> CoreExpr -> SpecType -> State CGInfo ()
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 -> State CGInfo ()
cconsE CGEnv
γ (CoreExpr -> CoreExpr
f CoreExpr
e) SpecType
t

cconsE' CGEnv
γ e :: CoreExpr
e@(Cast CoreExpr
e' CoercionR
c) SpecType
t
  = do t' <- (SpecType -> RReft -> SpecType
forall r v c tv.
Reftable r =>
RTypeV v c tv r -> r -> RTypeV v c tv r
`strengthen` Reft -> RReft
forall r v. r -> UReftV v r
uTop (SpecType -> Reft
forall r c tv. Reftable r => RType c tv r -> Reft
rTypeReft SpecType
t)) (SpecType -> SpecType) -> CG SpecType -> CG SpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CGEnv -> Type -> CoreExpr -> CoercionR -> CG SpecType
castTy CGEnv
γ (HasDebugCallStack => CoreExpr -> Type
CoreExpr -> Type
exprType CoreExpr
e) CoreExpr
e' CoercionR
c
       addC (SubC γ (F.notracepp ("Casted Type for " ++ GM.showPpr e ++ "\n init type " ++ showpp t) t') t) ("cconsE Cast: " ++ GM.showPpr e)

cconsE' CGEnv
γ CoreExpr
e SpecType
t
  = do te  <- CGEnv -> CoreExpr -> CG SpecType
consE CGEnv
γ CoreExpr
e
       te' <- instantiatePreds γ e te >>= addPost γ
       addC (SubC γ te' t) ("cconsE: " ++ "\n t = " ++ showpp t ++ "\n te = " ++ showpp te ++ GM.showPpr 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
  | CGEnv -> Bool
forall t. HasConfig t => t -> Bool
higherOrderFlag CGEnv
γ
  = do expr <- CGEnv -> CoreExpr -> CG (Maybe (ExprV Symbol))
lamExpr CGEnv
γ CoreExpr
e
       return $ case expr of
         Just ExprV Symbol
e' -> Reft -> RReft
forall r v. r -> UReftV v r
uTop (Reft -> RReft) -> Reft -> RReft
forall a b. (a -> b) -> a -> b
$ ExprV Symbol -> Reft
forall a. Expression a => a -> Reft
F.exprReft (ExprV Symbol -> Reft) -> ExprV Symbol -> Reft
forall a b. (a -> b) -> a -> b
$ (Symbol, Sort) -> ExprV Symbol -> ExprV Symbol
forall v. (Symbol, Sort) -> ExprV v -> ExprV v
F.ELam (Id -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Id
x, Sort
sx) ExprV Symbol
e'
         Maybe (ExprV Symbol)
_       -> RReft
forall a. Monoid a => a
mempty
  where
    sx :: Sort
sx = TCEmb TyCon -> Type -> Sort
typeSort TCEmb TyCon
tce (Type -> Sort) -> Type -> Sort
forall a b. (a -> b) -> a -> b
$ Type -> Type
Ghc.expandTypeSynonyms (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Id -> Type
varType Id
x
lambdaSingleton CGEnv
_ TCEmb TyCon
_ Id
_ CoreExpr
_
  = RReft -> CG RReft
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return RReft
forall a. Monoid a => a
mempty

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


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

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

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

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


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

--------------------------------------------------------------------------------
-- | Bidirectional Constraint Generation: SYNTHESIS ----------------------------
--------------------------------------------------------------------------------
consE :: CGEnv -> CoreExpr -> CG SpecType
--------------------------------------------------------------------------------
consE :: CGEnv -> CoreExpr -> CG SpecType
consE CGEnv
γ CoreExpr
e
  | CGEnv -> Bool
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
γ ([Char] -> Pattern -> Pattern
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"CONSE-PATTERN: " Pattern
p) (HasDebugCallStack => CoreExpr -> Type
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 t0 <- HasCallStack => CGEnv -> Id -> CG SpecType
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 = Symbol
selfSymbol Symbol -> [Symbol] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` SpecType -> [Symbol]
forall a. Subable a => a -> [Symbol]
F.syms SpecType
t0
       let t = if Bool
hasSelf
                then (Reft -> Reft) -> RReft -> RReft
forall a b. (a -> b) -> UReftV Symbol a -> UReftV Symbol b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Reft -> Reft
ignoreSelf (RReft -> RReft) -> SpecType -> SpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SpecType
t0
                else SpecType
t0
       addLocA (Just x) (getLocation γ) (varAnn γ x t)
       return t

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

consE CGEnv
_ (Lit Literal
c)
  = SpecType -> CG SpecType
forall (m :: * -> *). FreshM m => SpecType -> m SpecType
refreshVV (SpecType -> CG SpecType) -> SpecType -> CG SpecType
forall a b. (a -> b) -> a -> b
$ RType RTyCon RTyVar Reft -> SpecType
forall c tv a. RType c tv a -> RType c tv (UReft a)
uRType (RType RTyCon RTyVar Reft -> SpecType)
-> RType RTyCon RTyVar Reft -> SpecType
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 α te _ <- ([Char], CoreExpr) -> CGEnv -> SpecType -> SpecType
forall a.
Outputable a =>
([Char], a) -> CGEnv -> SpecType -> SpecType
checkAll ([Char]
"Non-all TyApp with expr", CoreExpr
e) CGEnv
γ (SpecType -> SpecType) -> CG SpecType -> CG SpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CGEnv -> CoreExpr -> CG SpecType
consE CGEnv
γ CoreExpr
e
       t            <- if not (nopolyinfer (getConfig γ)) && isPos α && isGenericVar (ty_var_value α) te
                         then freshTyType (typeclass (getConfig γ)) TypeInstE e τ
                         else trueTy (typeclass (getConfig γ)) τ
       addW          $ WfC γ t
       t'           <- refreshVV t
       tt0          <- instantiatePreds γ e' (subsTyVarMeet' (ty_var_value α, t') te)
       let tt        = CGEnv -> CoreExpr -> SpecType -> SpecType
makeSingleton CGEnv
γ (CoreExpr -> CoreExpr
simplify CoreExpr
e') (SpecType -> SpecType) -> SpecType -> SpecType
forall a b. (a -> b) -> a -> b
$ CGEnv -> RTyVar -> Type -> SpecType -> SpecType
subsTyReft CGEnv
γ (RTVar RTyVar (RType RTyCon RTyVar ()) -> RTyVar
forall tv s. RTVar tv s -> tv
ty_var_value RTVar RTyVar (RType RTyCon RTyVar ())
α) Type
τ SpecType
tt0
       return $ case rTVarToBind α of
         Just (Symbol
x, RType RTyCon RTyVar ()
_) -> SpecType
-> (ExprV Symbol -> SpecType) -> Maybe (ExprV Symbol) -> SpecType
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (CGEnv -> CoreExpr -> Symbol -> SpecType -> CoreExpr -> SpecType
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) (SpecType -> (Symbol, ExprV Symbol) -> SpecType
forall a. Subable a => a -> (Symbol, ExprV Symbol) -> a
F.subst1 SpecType
tt ((Symbol, ExprV Symbol) -> SpecType)
-> (ExprV Symbol -> (Symbol, ExprV Symbol))
-> ExprV Symbol
-> SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol
x,)) (Type -> Maybe (ExprV Symbol)
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 (CGEnv -> Config
forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)) Bool -> Bool -> Bool
|| RTVInfo s -> Bool
forall s. RTVInfo s -> Bool
rtv_is_pol (RTVar tv s -> RTVInfo s
forall tv s. RTVar tv s -> RTVInfo s
ty_var_info RTVar tv s
α)

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

consE CGEnv
γ e' :: CoreExpr
e'@(App CoreExpr
e CoreExpr
a)
  = do ([], πs, te) <- SpecType
-> ([(RTVar RTyVar (RType RTyCon RTyVar ()), RReft)],
    [PVarV Symbol (RType RTyCon RTyVar ())], SpecType)
forall v tv c r.
RTypeV v tv c r
-> ([(RTVar c (RTypeV v tv c ()), r)],
    [PVarV v (RTypeV v tv c ())], RTypeV v tv c r)
bkUniv (SpecType
 -> ([(RTVar RTyVar (RType RTyCon RTyVar ()), RReft)],
     [PVarV Symbol (RType RTyCon RTyVar ())], SpecType))
-> CG SpecType
-> StateT
     CGInfo
     Identity
     ([(RTVar RTyVar (RType RTyCon RTyVar ()), RReft)],
      [PVarV Symbol (RType RTyCon RTyVar ())], SpecType)
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
       te1        <- instantiatePreds γ e' $ foldr RAllP te πs
       (γ', te2)  <- dropExists γ te1
       te3        <- dropConstraints γ te2
       updateLocA (exprLoc e) te3
       let RFun x _ tx t _ = checkFun ("Non-fun App with caller ", e') γ te3
       cconsE γ' a tx
       makeSingleton γ' (simplify e') <$> addPost γ' (maybe (checkUnbound γ' e' x t a) (F.subst1 t . (x,)) (argExpr γ $ simplify a))

consE CGEnv
γ (Lam Id
α CoreExpr
e) | Id -> Bool
isTyVar Id
α
  = do γ' <- CGEnv -> Id -> CG CGEnv
updateEnvironment CGEnv
γ Id
α
       t' <- consE γ' e
       return $ RAllT (makeRTVar $ rTyVar α) t' mempty

consE CGEnv
γ  e :: CoreExpr
e@(Lam Id
x CoreExpr
e1)
  = do tx      <- Bool -> KVKind -> CoreExpr -> Type -> CG SpecType
freshTyType (Config -> Bool
typeclass (CGEnv -> Config
forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)) KVKind
LamE (Id -> CoreExpr
forall b. Id -> Expr b
Var Id
x) Type
τx
       γ'      <- γ += ("consE", F.symbol x, tx)
       t1      <- consE γ' e1
       addIdA x $ AnnDef tx
       addW     $ WfC γ tx
       tce     <- gets tyConEmbed
       lamSing <- lambdaSingleton γ tce x e1
       return   $ RFun (F.symbol x) (mkRFInfo $ getConfig γ) tx t1 lamSing
    where
      FunTy { ft_arg :: Type -> Type
ft_arg = Type
τx } = HasDebugCallStack => CoreExpr -> Type
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 (HasDebugCallStack => CoreExpr -> Type
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 t <- CGEnv -> CoreExpr -> CG SpecType
consE (CGEnv -> Span -> CGEnv
setLocation CGEnv
γ (CoreTickish -> Span
Sp.Tick CoreTickish
tt)) CoreExpr
e
       addLocA Nothing (GM.tickSrcSpan tt) (AnnUse t)
       return 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
γ (HasDebugCallStack => CoreExpr -> Type
CoreExpr -> Type
exprType CoreExpr
e) CoreExpr
e' CoercionR
c

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

consE CGEnv
_ e :: CoreExpr
e@(Type Type
t)
  = Maybe SrcSpan -> [Char] -> CG SpecType
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing ([Char] -> CG SpecType) -> [Char] -> CG SpecType
forall a b. (a -> b) -> a -> b
$ [Char]
"consE cannot handle type " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (CoreExpr, Type) -> [Char]
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 ([Alt Id] -> Int
forall a. [a] -> Int
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", Name -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (Name -> Symbol) -> Name -> Symbol
forall a b. (a -> b) -> a -> b
$ Id -> Name
varName Id
a, Type -> SpecType
forall r. Monoid r => Type -> RRType r
kindToRType (Type -> SpecType) -> Type -> SpecType
forall a b. (a -> b) -> a -> b
$ Id -> Type
tyVarKind Id
a)
  | Bool
otherwise
  = CGEnv -> CG CGEnv
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return CGEnv
γ

getExprFun :: CGEnv -> CoreExpr -> Var
getExprFun :: CGEnv -> CoreExpr -> Id
getExprFun CGEnv
γ CoreExpr
e          = CoreExpr -> Id
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
_                = Maybe SrcSpan -> [Char] -> Id
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic (SrcSpan -> Maybe SrcSpan
forall a. a -> Maybe a
Just (CGEnv -> SrcSpan
getLocation CGEnv
γ)) [Char]
msg
    msg :: [Char]
msg                 = [Char]
"getFunName on \t" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ CoreExpr -> [Char]
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
γ           =  CoreExpr -> Maybe Id
forall {b}. Expr b -> Maybe Id
go
  where
    go :: Expr b -> Maybe Id
go (Var Id
x)          = case DEnv Id SpecType -> Id -> Maybe (HashMap Symbol (RISig SpecType))
forall k t.
(Eq k, Hashable k) =>
DEnv k t -> k -> Maybe (HashMap Symbol (RISig t))
dlookup (CGEnv -> DEnv Id SpecType
denv CGEnv
γ) Id
x of {Just HashMap Symbol (RISig SpecType)
_ -> Id -> Maybe Id
forall a. a -> Maybe a
Just Id
x; Maybe (HashMap Symbol (RISig SpecType))
Nothing -> Maybe Id
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
_                = Maybe Id
forall a. Maybe a
Nothing

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

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

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

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

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

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

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

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

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

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

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

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

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

--------------------------------------------------------------------------------
castTy  :: CGEnv -> Type -> CoreExpr -> Coercion -> CG SpecType
castTy' :: CGEnv -> Type -> CoreExpr -> CG SpecType
--------------------------------------------------------------------------------
castTy :: CGEnv -> Type -> CoreExpr -> CoercionR -> CG SpecType
castTy CGEnv
γ Type
t CoreExpr
e (AxiomInstCo CoAxiom Branched
ca Int
_ [CoercionR]
_)
  = SpecType -> Maybe SpecType -> SpecType
forall a. a -> Maybe a -> a
fromMaybe (SpecType -> Maybe SpecType -> SpecType)
-> CG SpecType
-> StateT CGInfo Identity (Maybe SpecType -> SpecType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CGEnv -> Type -> CoreExpr -> CG SpecType
castTy' CGEnv
γ Type
t CoreExpr
e StateT CGInfo Identity (Maybe SpecType -> SpecType)
-> StateT CGInfo Identity (Maybe SpecType) -> CG SpecType
forall a b.
StateT CGInfo Identity (a -> b)
-> StateT CGInfo Identity a -> StateT CGInfo Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TyCon -> StateT CGInfo Identity (Maybe SpecType)
lookupNewType (CoAxiom Branched -> TyCon
forall (br :: BranchFlag). CoAxiom br -> TyCon
coAxiomTyCon CoAxiom Branched
ca)

castTy CGEnv
γ Type
t CoreExpr
e (SymCo (AxiomInstCo CoAxiom Branched
ca Int
_ [CoercionR]
_))
  = do mtc <- TyCon -> StateT CGInfo Identity (Maybe SpecType)
lookupNewType (CoAxiom Branched -> TyCon
forall (br :: BranchFlag). CoAxiom br -> TyCon
coAxiomTyCon CoAxiom Branched
ca)
       F.forM_ mtc (cconsE γ e)
       castTy' γ t 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 t0 <- Bool -> Type -> CG SpecType
trueTy (Config -> Bool
typeclass (CGEnv -> Config
forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)) Type
τ
       tx <- varRefType γ x
       let t = SpecType -> SpecType -> SpecType
mergeCastTys SpecType
t0 SpecType
tx
       let ce = if Config -> Bool
typeclass (CGEnv -> Config
forall t. HasConfig t => t -> Config
getConfig CGEnv
γ) Bool -> Bool -> Bool
&& Config -> Bool
noADT (CGEnv -> Config
forall t. HasConfig t => t -> Config
getConfig CGEnv
γ) then Id -> ExprV Symbol
forall a. Expression a => a -> ExprV Symbol
F.expr Id
x
                  else Sort -> Sort -> ExprV Symbol -> ExprV Symbol
forall {v}. Sort -> Sort -> ExprV v -> ExprV v
eCoerc (TCEmb TyCon -> Type -> Sort
typeSort (CGEnv -> TCEmb TyCon
emb CGEnv
γ) (Type -> Sort) -> Type -> Sort
forall a b. (a -> b) -> a -> b
$ Type -> Type
Ghc.expandTypeSynonyms (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Id -> Type
varType Id
x)
                         (TCEmb TyCon -> Type -> Sort
typeSort (CGEnv -> TCEmb TyCon
emb CGEnv
γ) Type
τ)
                         (ExprV Symbol -> ExprV Symbol) -> ExprV Symbol -> ExprV Symbol
forall a b. (a -> b) -> a -> b
$ Id -> ExprV Symbol
forall a. Expression a => a -> ExprV Symbol
F.expr Id
x
       return (t `strengthen` uTop (F.uexprReft ce) {- `meet` tx -})
  where eCoerc :: Sort -> Sort -> ExprV v -> ExprV v
eCoerc Sort
s Sort
t ExprV v
e
         | Sort
s Sort -> Sort -> Bool
forall a. Eq a => a -> a -> Bool
== Sort
t    = ExprV v
e
         | Bool
otherwise = Sort -> Sort -> ExprV v -> ExprV v
forall {v}. Sort -> Sort -> ExprV v -> ExprV v
F.ECoerc Sort
s Sort
t ExprV v
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
  = Maybe SrcSpan -> [Char] -> CG SpecType
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing ([Char] -> CG SpecType) -> [Char] -> CG SpecType
forall a b. (a -> b) -> a -> b
$ [Char]
"castTy cannot handle expr " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ CoreExpr -> [Char]
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
  | Bool -> SpecType -> Type
forall r. ToTypeable r => Bool -> RRType r -> Type
toType Bool
False SpecType
t1 Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Bool -> SpecType -> Type
forall r. ToTypeable r => Bool -> RRType r -> Type
toType Bool
False SpecType
t2
  = SpecType
t2
mergeCastTys (RApp RTyCon
c1 [SpecType]
ts1 [RTProp RTyCon RTyVar RReft]
ps1 RReft
r1) (RApp RTyCon
c2 [SpecType]
ts2 [RTProp RTyCon RTyVar RReft]
_ RReft
_)
  | RTyCon
c1 RTyCon -> RTyCon -> Bool
forall a. Eq a => a -> a -> Bool
== RTyCon
c2
  = RTyCon
-> [SpecType] -> [RTProp RTyCon RTyVar RReft] -> RReft -> SpecType
forall v c tv r.
c
-> [RTypeV v c tv r] -> [RTPropV v c tv r] -> r -> RTypeV v c tv r
RApp RTyCon
c1 ((SpecType -> SpecType -> SpecType)
-> [SpecType] -> [SpecType] -> [SpecType]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith SpecType -> SpecType -> SpecType
mergeCastTys [SpecType]
ts1 [SpecType]
ts2) [RTProp RTyCon RTyVar RReft]
ps1 RReft
r1
mergeCastTys SpecType
t SpecType
_
  = SpecType
t

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

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

  | Bool
otherwise
  = Maybe (CoreExpr -> CoreExpr)
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
  t   <- Bool -> KVKind -> CoreExpr -> Type -> CG SpecType
freshTyType (Config -> Bool
typeclass (CGEnv -> Config
forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)) KVKind
kvkind CoreExpr
e (Type -> CG SpecType) -> Type -> CG SpecType
forall a b. (a -> b) -> a -> b
$ HasDebugCallStack => CoreExpr -> Type
CoreExpr -> Type
exprType CoreExpr
e
  addW $ WfC γ t
  cconsE γ e t
  return 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 Symbol -> [Symbol] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` a -> [Symbol]
forall a. Subable a => a -> [Symbol]
F.syms a
t = a
t
  | Bool
otherwise            = Maybe SrcSpan -> [Char] -> a
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic (SrcSpan -> Maybe SrcSpan
forall a. a -> Maybe a
Just (SrcSpan -> Maybe SrcSpan) -> SrcSpan -> Maybe SrcSpan
forall a b. (a -> b) -> a -> b
$ CGEnv -> SrcSpan
getLocation CGEnv
γ) [Char]
msg
  where
    msg :: [Char]
msg = [[Char]] -> [Char]
unlines [ [Char]
"checkUnbound: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Symbol -> [Char]
forall a. Show a => a -> [Char]
show Symbol
x [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" is elem of syms of " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. Show a => a -> [Char]
show a
t
                  , [Char]
"In"
                  , CoreExpr -> [Char]
forall a. Outputable a => a -> [Char]
GM.showPpr CoreExpr
e
                  , [Char]
"Arg = "
                  , a2 -> [Char]
forall a. Show a => a -> [Char]
show a2
a
                  ]

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

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

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

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

{-

case x :: List b of
  Emp -> e

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

-}
-------------------------------------------------------------------------------------
caseEnv   :: CGEnv -> Var -> [AltCon] -> AltCon -> [Var] -> Maybe [Int] -> CG CGEnv
-------------------------------------------------------------------------------------
caseEnv :: CGEnv
-> 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')   = Id -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (Id -> Symbol) -> [Id] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Id
xId -> [Id] -> [Id]
forall a. a -> [a] -> [a]
:[Id]
ys)
  xt0             <- ([Char], Id) -> CGEnv -> SpecType -> SpecType
forall a.
Outputable a =>
([Char], a) -> CGEnv -> SpecType -> SpecType
checkTyCon ([Char]
"checkTycon cconsCase", Id
x) CGEnv
γ (SpecType -> SpecType) -> CG SpecType -> CG SpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CGEnv
γ HasCallStack => CGEnv -> Id -> CG SpecType
CGEnv -> Id -> CG SpecType
??= Id
x
  let rt           = SpecType -> Symbol -> SpecType
forall c (f :: * -> *) tv.
(TyConable c, Reftable (f Reft), Functor f) =>
RType c tv (f Reft) -> Symbol -> RType c tv (f Reft)
shiftVV SpecType
xt0 Symbol
x'
  tdc             <- γ ??= dataConWorkId c >>= refreshVV
  let (rtd,yts',_) = unfoldR tdc rt ys
  yts             <- projectTypes (typeclass (getConfig γ))  pIs yts'
  let ys''         = Id -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (Id -> Symbol) -> [Id] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Id -> Bool) -> [Id] -> [Id]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Id -> Bool) -> Id -> Bool
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           = DataCon -> [Symbol] -> Reft
dataConReft   DataCon
c   [Symbol]
ys''
  let r2           = SpecType -> [Symbol] -> Reft
forall r c tv. Reftable r => RType c tv r -> [Symbol] -> Reft
dataConMsReft SpecType
rtd [Symbol]
ys''
  let xt           = (SpecType
xt0 SpecType -> SpecType -> SpecType
forall r. Reftable r => r -> r -> r
`meet` SpecType
rtd) SpecType -> RReft -> SpecType
forall r v c tv.
Reftable r =>
RTypeV v c tv r -> r -> RTypeV v c tv r
`strengthen` Reft -> RReft
forall r v. r -> UReftV v r
uTop (Reft
r1 Reft -> Reft -> Reft
forall r. Reftable r => r -> r -> r
`meet` Reft
r2)
  let cbs          = [Char] -> [Symbol] -> [SpecType] -> [(Symbol, SpecType)]
forall a b. HasCallStack => [Char] -> [a] -> [b] -> [(a, b)]
safeZip [Char]
"cconsCase" (Symbol
x'Symbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
:[Symbol]
ys')
                         ((SpecType -> SpecType) -> [SpecType] -> [SpecType]
forall a b. (a -> b) -> [a] -> [b]
map (SpecType -> (Symbol, ExprV Symbol) -> SpecType
forall a. Subable a => a -> (Symbol, ExprV Symbol) -> a
`F.subst1` (Symbol
selfSymbol, Symbol -> ExprV Symbol
forall v. v -> ExprV v
F.EVar Symbol
x'))
                         (SpecType
xt0 SpecType -> [SpecType] -> [SpecType]
forall a. a -> [a] -> [a]
: [SpecType]
yts))
  cγ'  <- addBinders γ   x' cbs
  when allowDC $
    addRewritesForNextBinding $ getCaseRewrites γ $ xt0 `meet` rtd
  addBinders cγ' x' [(x', substSelf <$> xt)]
  where allowTC :: Bool
allowTC    = Config -> Bool
typeclass (CGEnv -> Config
forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)
        allowDC :: Bool
allowDC    = Config -> Bool
dependantCase (CGEnv -> Config
forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)

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


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

substSelf :: UReft F.Reft -> UReft F.Reft
substSelf :: RReft -> RReft
substSelf (MkUReft Reft
r PredicateV Symbol
p) = Reft -> PredicateV Symbol -> RReft
forall v r. r -> PredicateV v -> UReftV v r
MkUReft (Reft -> Reft
substSelfReft Reft
r) PredicateV Symbol
p

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

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

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

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

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

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

instantiateTys :: SpecType -> [SpecType] -> SpecType
instantiateTys :: SpecType -> [SpecType] -> SpecType
instantiateTys = (SpecType -> SpecType -> SpecType)
-> SpecType -> [SpecType] -> SpecType
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' SpecType -> SpecType -> SpecType
forall {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 ()))) =>
RTypeV Symbol c tv r
-> RTypeV Symbol c tv r -> RTypeV Symbol c tv r
go
  where
    go :: RTypeV Symbol c tv r
-> RTypeV Symbol c tv r -> RTypeV Symbol c tv r
go (RAllT RTVar tv (RType c tv ())
α RTypeV Symbol c tv r
tbody r
_) RTypeV Symbol c tv r
t = (tv, RTypeV Symbol c tv r)
-> RTypeV Symbol c tv r -> RTypeV Symbol c tv 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' (RTVar tv (RType c tv ()) -> tv
forall tv s. RTVar tv s -> tv
ty_var_value RTVar tv (RType c tv ())
α, RTypeV Symbol c tv r
t) RTypeV Symbol c tv r
tbody
    go RTypeV Symbol c tv r
_ RTypeV Symbol c tv r
_                 = Maybe SrcSpan -> [Char] -> RTypeV Symbol c tv r
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing [Char]
"Constraint.instantiateTy"

instantiatePvs :: SpecType -> [SpecProp] -> SpecType
instantiatePvs :: SpecType -> [RTProp RTyCon RTyVar RReft] -> SpecType
instantiatePvs           = (SpecType -> RTProp RTyCon RTyVar RReft -> SpecType)
-> SpecType -> [RTProp RTyCon RTyVar RReft] -> SpecType
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' SpecType -> RTProp RTyCon RTyVar RReft -> SpecType
go
  where
    go :: SpecType -> RTProp RTyCon RTyVar RReft -> SpecType
go (RAllP PVarV Symbol (RType RTyCon RTyVar ())
p SpecType
tbody) RTProp RTyCon RTyVar RReft
r = [Char]
-> SpecType
-> [(PVarV Symbol (RType RTyCon RTyVar ()),
     RTProp RTyCon RTyVar RReft)]
-> SpecType
replacePreds [Char]
"instantiatePv" SpecType
tbody [(PVarV Symbol (RType RTyCon RTyVar ())
p, RTProp RTyCon RTyVar RReft
r)]
    go SpecType
t               RTProp RTyCon RTyVar RReft
_ = [Char] -> [Char] -> SpecType
forall a. [Char] -> [Char] -> a
errorP [Char]
"" ([Char]
"Constraint.instantiatePvs: t = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SpecType -> [Char]
forall a. PPrint a => a -> [Char]
showpp SpecType
t)

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

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

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

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

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

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

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


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


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

--------------------------------------------------------------------------------
(??=) :: (?callStack :: CallStack) => CGEnv -> Var -> CG SpecType
--------------------------------------------------------------------------------
CGEnv
γ ??= :: HasCallStack => CGEnv -> Id -> CG SpecType
??= Id
x = case Symbol -> HashMap Symbol CoreExpr -> Maybe CoreExpr
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 -> SpecType -> CG SpecType
forall (m :: * -> *). FreshM m => SpecType -> m SpecType
refreshTy SpecType
tx
          where
            x' :: Symbol
x' = Id -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Id
x
            tx :: SpecType
tx = SpecType -> Maybe SpecType -> SpecType
forall a. a -> Maybe a -> a
fromMaybe SpecType
forall {r}. Monoid r => RRType r
tt (CGEnv
γ HasCallStack => CGEnv -> Symbol -> Maybe SpecType
CGEnv -> Symbol -> Maybe SpecType
?= Symbol
x')
            tt :: RRType r
tt = Type -> RRType r
forall r. Monoid r => Type -> RRType r
ofType (Type -> RRType r) -> Type -> RRType r
forall a b. (a -> b) -> a -> b
$ Id -> Type
varType Id
x


--------------------------------------------------------------------------------
varRefType :: (?callStack :: CallStack) => CGEnv -> Var -> CG SpecType
--------------------------------------------------------------------------------
varRefType :: HasCallStack => CGEnv -> Id -> CG SpecType
varRefType CGEnv
γ Id
x =
  CGEnv -> Id -> SpecType -> SpecType
varRefType' CGEnv
γ Id
x (SpecType -> SpecType) -> CG SpecType -> CG SpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (CGEnv
γ HasCallStack => CGEnv -> Id -> CG SpecType
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  <- Symbol -> HashMap Symbol SpecType -> Maybe SpecType
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup Symbol
x' HashMap Symbol SpecType
tys
  = SpecType -> RReft -> SpecType
forall {r} {c} {tv}.
(PPrint r, Reftable r) =>
RType c tv r -> r -> RType c tv r
strengthen' SpecType
tr RReft
xr
  | Bool
otherwise
  = SpecType -> RReft -> SpecType
forall {r} {c} {tv}.
(PPrint r, Reftable r) =>
RType c tv r -> r -> RType c tv r
strengthen' SpecType
t' RReft
xr
  where
    xr :: RReft
xr = Id -> RReft
forall a. Symbolic a => a -> RReft
singletonReft Id
x
    x' :: Symbol
x' = Id -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Id
x
    strengthen' :: RType c tv r -> r -> RType c tv r
strengthen' | CGEnv -> Bool
forall t. HasConfig t => t -> Bool
higherOrderFlag CGEnv
γ = RType c tv r -> r -> RType c tv r
forall {r} {c} {tv}.
(PPrint r, Reftable r) =>
RType c tv r -> r -> RType c tv r
strengthenMeet
                | Bool
otherwise         = RType c tv r -> r -> RType c tv r
forall {r} {c} {tv}.
(PPrint r, 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
  | CGEnv -> Bool
forall t. HasConfig t => t -> Bool
higherOrderFlag CGEnv
γ, App CoreExpr
f CoreExpr
x <- CoreExpr -> CoreExpr
simplify CoreExpr
cexpr
  = case (CGEnv -> CoreExpr -> Maybe (ExprV Symbol)
funExpr CGEnv
γ CoreExpr
f, CoreExpr -> Maybe (ExprV Symbol)
argForAllExpr CoreExpr
x) of
      (Just ExprV Symbol
f', Just ExprV Symbol
x')
                 | Bool -> Bool
not (if Config -> Bool
typeclass (CGEnv -> Config
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)
                 -> SpecType -> RReft -> SpecType
forall {r} {c} {tv}.
(PPrint r, Reftable r) =>
RType c tv r -> r -> RType c tv r
strengthenMeet SpecType
t (Reft -> RReft
forall r v. r -> UReftV v r
uTop (Reft -> RReft) -> Reft -> RReft
forall a b. (a -> b) -> a -> b
$ ExprV Symbol -> Reft
forall a. Expression a => a -> Reft
F.exprReft (ExprV Symbol -> ExprV Symbol -> ExprV Symbol
forall v. ExprV v -> ExprV v -> ExprV v
F.EApp ExprV Symbol
f' ExprV Symbol
x'))
      (Just ExprV Symbol
f', Just ExprV Symbol
_)
                 -> SpecType -> RReft -> SpecType
forall {r} {c} {tv}.
(PPrint r, Reftable r) =>
RType c tv r -> r -> RType c tv r
strengthenMeet SpecType
t (Reft -> RReft
forall r v. r -> UReftV v r
uTop (Reft -> RReft) -> Reft -> RReft
forall a b. (a -> b) -> a -> b
$ ExprV Symbol -> Reft
forall a. Expression a => a -> Reft
F.exprReft ExprV Symbol
f')
      (Maybe (ExprV Symbol), Maybe (ExprV Symbol))
_ -> SpecType
t
  | Config -> Bool
rankNTypes (CGEnv -> Config
forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)
  = case CGEnv -> CoreExpr -> Maybe (ExprV Symbol)
argExpr CGEnv
γ (CoreExpr -> CoreExpr
simplify CoreExpr
cexpr) of
       Just ExprV Symbol
e' -> SpecType -> RReft -> SpecType
forall {r} {c} {tv}.
(PPrint r, Reftable r) =>
RType c tv r -> r -> RType c tv r
strengthenMeet SpecType
t (RReft -> SpecType) -> RReft -> SpecType
forall a b. (a -> b) -> a -> b
$ Reft -> RReft
forall r v. r -> UReftV v r
uTop (ExprV Symbol -> Reft
forall a. Expression a => a -> Reft
F.exprReft ExprV Symbol
e')
       Maybe (ExprV Symbol)
_       -> SpecType
t
  | Bool
otherwise
  = SpecType
t
  where
    argForAllExpr :: CoreExpr -> Maybe (ExprV Symbol)
argForAllExpr (Var Id
x)
      | Config -> Bool
rankNTypes (CGEnv -> Config
forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)
      , Just ExprV Symbol
e <- Id -> HashMap Id (ExprV Symbol) -> Maybe (ExprV Symbol)
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup Id
x (CGEnv -> HashMap Id (ExprV Symbol)
forallcb CGEnv
γ)
      = ExprV Symbol -> Maybe (ExprV Symbol)
forall a. a -> Maybe a
Just ExprV Symbol
e
    argForAllExpr CoreExpr
e
      = CGEnv -> CoreExpr -> Maybe (ExprV Symbol)
argExpr CGEnv
γ CoreExpr
e



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

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

funExpr CGEnv
γ (App CoreExpr
e1 CoreExpr
e2)
  = case (CGEnv -> CoreExpr -> Maybe (ExprV Symbol)
funExpr CGEnv
γ CoreExpr
e1, CGEnv -> CoreExpr -> Maybe (ExprV Symbol)
argExpr CGEnv
γ CoreExpr
e2) of
      (Just ExprV Symbol
e1', Just ExprV Symbol
e2') | Bool -> Bool
not (if Config -> Bool
typeclass (CGEnv -> Config
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)
                           -> ExprV Symbol -> Maybe (ExprV Symbol)
forall a. a -> Maybe a
Just (ExprV Symbol -> ExprV Symbol -> ExprV Symbol
forall v. ExprV v -> ExprV v -> ExprV v
F.EApp ExprV Symbol
e1' ExprV Symbol
e2')
      (Just ExprV Symbol
e1', Just ExprV Symbol
_)   -> ExprV Symbol -> Maybe (ExprV Symbol)
forall a. a -> Maybe a
Just ExprV Symbol
e1'
      (Maybe (ExprV Symbol), Maybe (ExprV Symbol))
_                    -> Maybe (ExprV Symbol)
forall a. Maybe a
Nothing

funExpr CGEnv
_ CoreExpr
_
  = Maybe (ExprV Symbol)
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)           = CoreExpr -> CoreExpr -> CoreExpr
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 = Reft -> RReft
forall r v. r -> UReftV v r
uTop (Reft -> RReft) -> (a -> Reft) -> a -> RReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Reft
forall a. Symbolic a => a -> Reft
F.symbolReft (Symbol -> Reft) -> (a -> Symbol) -> a -> Reft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol

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

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

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

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

isType :: Expr CoreBndr -> Bool
isType :: CoreExpr -> Bool
isType (Type Type
_)                 = Bool
True
isType CoreExpr
a                        = Type -> Type -> Bool
eqType (HasDebugCallStack => CoreExpr -> Type
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 =  ((Class, RTyVar) -> Bool) -> [(Class, RTyVar)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\(Class
c, RTyVar
α') -> (RTyVar
α'RTyVar -> RTyVar -> Bool
forall a. Eq a => a -> a -> Bool
/=RTyVar
α) Bool -> Bool -> Bool
|| Class -> Bool
isGenericClass Class
c ) (SpecType -> [(Class, RTyVar)]
forall {b} {r}.
(PPrint b, PPrint r, Reftable r, Reftable (RTProp RTyCon b r),
 Reftable (RTProp RTyCon b ()), Hashable b, FreeVar RTyCon b,
 SubsTy b (RType RTyCon b ()) b, SubsTy b (RType RTyCon b ()) r,
 SubsTy b (RType RTyCon b ()) (RType RTyCon b ()),
 SubsTy b (RType RTyCon b ()) (RTVar b (RType RTyCon b ())),
 SubsTy b (RType RTyCon b ()) RTyCon) =>
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, RTVar b (RType RTyCon b ()) -> b
forall tv s. RTVar tv s -> tv
ty_var_value RTVar b (RType RTyCon b ())
α')
                        | (Class
c, [RType RTyCon b r]
ts) <- RType RTyCon b r -> [(Class, [RType RTyCon b r])]
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 ())
α'      <- RType RTyCon b r -> [RTVar b (RType RTyCon b ())]
forall tv v c r.
Eq tv =>
RTypeV v c tv r -> [RTVar tv (RTypeV v c tv ())]
freeTyVars RType RTyCon b r
t']
    isGenericClass :: Class -> Bool
isGenericClass Class
c = Class -> Name
className Class
c Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name
ordClassName, Name
eqClassName] -- , functorClassName, monadClassName]

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

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