{-# 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 #-}
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
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, mapSnd, safeZip )
import Language.Fixpoint.Types.Visitor
import qualified Language.Fixpoint.Types as F
import qualified Language.Fixpoint.Types.Visitor as F
import Language.Haskell.Liquid.Constraint.Fresh ( addKuts, freshTyType, trueTy )
import Language.Haskell.Liquid.Constraint.Init ( initEnv, initCGI )
import Language.Haskell.Liquid.Constraint.Env
import Language.Haskell.Liquid.Constraint.Monad
import Language.Haskell.Liquid.Constraint.Split ( splitC, splitW )
import Language.Haskell.Liquid.Constraint.Relational (consAssmRel, consRelTop)
import Language.Haskell.Liquid.Types hiding (binds, Loc, loc, Def)
import Language.Haskell.Liquid.Constraint.Types
import Language.Haskell.Liquid.Constraint.Constraint ( addConstraints )
import Language.Haskell.Liquid.Constraint.Template
import Language.Haskell.Liquid.Constraint.Termination
import Language.Haskell.Liquid.Transforms.CoreToLogic (weakenResult, runToLogic, coreToLogic)
import Language.Haskell.Liquid.Bare.DataType (dataConMap, makeDataConChecker)
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 { CGEnv
γ <- TargetInfo -> CG CGEnv
initEnv TargetInfo
info; CGEnv -> Config -> TargetInfo -> State CGInfo ()
consAct CGEnv
γ Config
cfg TargetInfo
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
γ' <- (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)
(PrEnv
ψ, CGEnv
γ'') <- ((PrEnv, CGEnv)
-> (Id, Id, Located SpecType, Located SpecType, RelExpr, RelExpr)
-> StateT CGInfo Identity (PrEnv, CGEnv))
-> (PrEnv, CGEnv)
-> [(Id, Id, Located SpecType, Located SpecType, RelExpr, RelExpr)]
-> StateT CGInfo Identity (PrEnv, CGEnv)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (Config
-> TargetInfo
-> (PrEnv, CGEnv)
-> (Id, Id, Located SpecType, Located SpecType, RelExpr, RelExpr)
-> StateT CGInfo Identity (PrEnv, CGEnv)
consAssmRel Config
cfg TargetInfo
info) ([], CGEnv
γ') (GhcSpecSig
-> [(Id, Id, Located SpecType, Located SpecType, RelExpr, RelExpr)]
gsAsmRel GhcSpecSig
sSpc [(Id, Id, Located SpecType, Located SpecType, RelExpr, RelExpr)]
-> [(Id, Id, Located SpecType, Located SpecType, RelExpr, RelExpr)]
-> [(Id, Id, Located SpecType, Located SpecType, RelExpr, RelExpr)]
forall a. [a] -> [a] -> [a]
++ GhcSpecSig
-> [(Id, Id, Located SpecType, Located SpecType, RelExpr, RelExpr)]
gsRelation GhcSpecSig
sSpc)
((Id, Id, Located SpecType, Located SpecType, RelExpr, RelExpr)
-> State CGInfo ())
-> [(Id, Id, Located SpecType, Located SpecType, RelExpr, RelExpr)]
-> State CGInfo ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Config
-> TargetInfo
-> CGEnv
-> PrEnv
-> (Id, Id, Located SpecType, Located SpecType, RelExpr, RelExpr)
-> State CGInfo ()
consRelTop Config
cfg TargetInfo
info CGEnv
γ'' PrEnv
ψ) (GhcSpecSig
-> [(Id, Id, Located SpecType, Located SpecType, RelExpr, RelExpr)]
gsRelation GhcSpecSig
sSpc)
((Id, MethodType (Located SpecType)) -> State CGInfo ())
-> [(Id, MethodType (Located SpecType))] -> State CGInfo ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (CGEnv -> (Id, MethodType (Located SpecType)) -> State CGInfo ()
consClass CGEnv
γ) (GhcSpecSig -> [(Id, MethodType (Located SpecType))]
gsMethods (GhcSpecSig -> [(Id, MethodType (Located SpecType))])
-> GhcSpecSig -> [(Id, MethodType (Located SpecType))]
forall a b. (a -> b) -> a -> b
$ TargetSpec -> GhcSpecSig
gsSig (TargetSpec -> GhcSpecSig) -> TargetSpec -> GhcSpecSig
forall a b. (a -> b) -> a -> b
$ TargetInfo -> TargetSpec
giSpec TargetInfo
info)
[SubC]
hcs <- (CGInfo -> [SubC]) -> StateT CGInfo Identity [SubC]
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CGInfo -> [SubC]
hsCs
[WfC]
hws <- (CGInfo -> [WfC]) -> StateT CGInfo Identity [WfC]
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CGInfo -> [WfC]
hsWfs
[FixSubC]
fcs <- [[FixSubC]] -> [FixSubC]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[FixSubC]] -> [FixSubC])
-> StateT CGInfo Identity [[FixSubC]]
-> StateT CGInfo Identity [FixSubC]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (SubC -> StateT CGInfo Identity [FixSubC])
-> [SubC] -> StateT CGInfo Identity [[FixSubC]]
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 -> SubC -> StateT CGInfo Identity [FixSubC]
splitC (Config -> Bool
typeclass (TargetInfo -> Config
forall t. HasConfig t => t -> Config
getConfig TargetInfo
info))) [SubC]
hcs
[FixWfC]
fws <- [[FixWfC]] -> [FixWfC]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[FixWfC]] -> [FixWfC])
-> StateT CGInfo Identity [[FixWfC]]
-> StateT CGInfo Identity [FixWfC]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (WfC -> StateT CGInfo Identity [FixWfC])
-> [WfC] -> StateT CGInfo Identity [[FixWfC]]
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 WfC -> StateT CGInfo Identity [FixWfC]
splitW [WfC]
hws
(CGInfo -> CGInfo) -> State CGInfo ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((CGInfo -> CGInfo) -> State CGInfo ())
-> (CGInfo -> CGInfo) -> State CGInfo ()
forall a b. (a -> b) -> a -> b
$ \CGInfo
st -> CGInfo
st { fEnv = fEnv st `mappend` feEnv (fenv γ)
, cgLits = litEnv γ
, cgConsts = cgConsts st `mappend` constEnv γ
, fixCs = fcs
, fixWfs = fws }
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
Bool
oldtcheck <- (CGInfo -> Bool) -> StateT CGInfo Identity Bool
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CGInfo -> Bool
tcheck
Bool
isStr <- Config -> CoreBind -> StateT CGInfo Identity Bool
doTermCheck (CGEnv -> Config
forall t. HasConfig t => t -> Config
getConfig CGEnv
γ) CoreBind
cb
(CGInfo -> CGInfo) -> State CGInfo ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((CGInfo -> CGInfo) -> State CGInfo ())
-> (CGInfo -> CGInfo) -> State CGInfo ()
forall a b. (a -> b) -> a -> b
$ \CGInfo
s -> CGInfo
s { tcheck = oldtcheck && isStr }
CGEnv
γ' <- TCheck -> CGEnv -> CoreBind -> CG CGEnv
consCB (Bool -> Bool -> TCheck
mkTCheck Bool
oldtcheck Bool
isStr) CGEnv
γ CoreBind
cb
(CGInfo -> CGInfo) -> State CGInfo ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((CGInfo -> CGInfo) -> State CGInfo ())
-> (CGInfo -> CGInfo) -> State CGInfo ()
forall a b. (a -> b) -> a -> b
$ \CGInfo
s -> CGInfo
s{tcheck = oldtcheck}
CGEnv -> CG CGEnv
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return CGEnv
γ'
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 Bool
oldtcheck <- (CGInfo -> Bool) -> StateT CGInfo Identity Bool
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CGInfo -> Bool
tcheck
Bool
isStr <- Config -> CoreBind -> StateT CGInfo Identity Bool
doTermCheck (CGEnv -> Config
forall t. HasConfig t => t -> Config
getConfig CGEnv
γ) CoreBind
cb
(CGInfo -> CGInfo) -> State CGInfo ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((CGInfo -> CGInfo) -> State CGInfo ())
-> (CGInfo -> CGInfo) -> State CGInfo ()
forall a b. (a -> b) -> a -> b
$ \CGInfo
s -> CGInfo
s { tcheck = oldtcheck && isStr}
let (CGEnv
γ', RTyConInv
i) = CGEnv -> CoreBind -> (CGEnv, RTyConInv)
removeInvariant CGEnv
γ CoreBind
cb
CGEnv
γ'' <- TCheck -> CGEnv -> CoreBind -> CG CGEnv
consCB (Bool -> Bool -> TCheck
mkTCheck Bool
oldtcheck Bool
isStr) (CGEnv
γ'{cgVar = topBind cb}) CoreBind
cb
(CGInfo -> CGInfo) -> State CGInfo ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((CGInfo -> CGInfo) -> State CGInfo ())
-> (CGInfo -> CGInfo) -> State CGInfo ()
forall a b. (a -> b) -> a -> b
$ \CGInfo
s -> CGInfo
s { tcheck = oldtcheck}
CGEnv -> CG CGEnv
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (CGEnv -> CG CGEnv) -> CGEnv -> CG CGEnv
forall a b. (a -> b) -> a -> b
$ CGEnv -> RTyConInv -> CGEnv
restoreInvariant CGEnv
γ'' RTyConInv
i
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
consCB :: TCheck -> CGEnv -> CoreBind -> CG CGEnv
consCB TCheck
TerminationCheck CGEnv
γ (Rec [(Id, CoreExpr)]
xes)
= do HashMap Id [Located Expr]
texprs <- (CGInfo -> HashMap Id [Located Expr])
-> StateT CGInfo Identity (HashMap Id [Located Expr])
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CGInfo -> HashMap Id [Located Expr]
termExprs
(CGInfo -> CGInfo) -> State CGInfo ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((CGInfo -> CGInfo) -> State CGInfo ())
-> (CGInfo -> CGInfo) -> State CGInfo ()
forall a b. (a -> b) -> a -> b
$ \CGInfo
i -> CGInfo
i { recCount = recCount i + length xes }
let xxes :: [(Id, [Located Expr])]
xxes = (Id -> Maybe (Id, [Located Expr]))
-> [Id] -> [(Id, [Located Expr])]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (Id -> HashMap Id [Located Expr] -> Maybe (Id, [Located Expr])
forall {k} {a}. Hashable k => k -> HashMap k a -> Maybe (k, a)
`lookup'` HashMap Id [Located Expr]
texprs) [Id]
xs
if [(Id, [Located Expr])] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Id, [Located Expr])]
xxes
then (Bool
-> CGEnv
-> (Id, CoreExpr, Template SpecType)
-> CG (Template SpecType))
-> CGEnv -> [(Id, CoreExpr)] -> CG CGEnv
consCBSizedTys Bool
-> CGEnv
-> (Id, CoreExpr, Template SpecType)
-> CG (Template SpecType)
consBind CGEnv
γ [(Id, CoreExpr)]
xes
else [(Id, [Located Expr])] -> CGEnv -> CGEnv
forall {t :: * -> *} {a} {p}. Foldable t => t a -> p -> p
check [(Id, [Located Expr])]
xxes (CGEnv -> CGEnv) -> CG CGEnv -> CG CGEnv
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Bool
-> CGEnv
-> (Id, CoreExpr, Template SpecType)
-> CG (Template SpecType))
-> CGEnv -> [(Id, CoreExpr)] -> CG CGEnv
consCBWithExprs Bool
-> CGEnv
-> (Id, CoreExpr, Template SpecType)
-> CG (Template SpecType)
consBind CGEnv
γ [(Id, CoreExpr)]
xes
where
xs :: [Id]
xs = ((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. 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. (?callStack::CallStack) => [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
consCB TCheck
StrataCheck CGEnv
γ (Rec [(Id, CoreExpr)]
xes)
= do [(Id, CoreExpr, Template SpecType)]
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)
(CGInfo -> CGInfo) -> State CGInfo ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((CGInfo -> CGInfo) -> State CGInfo ())
-> (CGInfo -> CGInfo) -> State CGInfo ()
forall a b. (a -> b) -> a -> b
$ \CGInfo
i -> CGInfo
i { recCount = recCount i + length xes }
let xts :: [(Id, Template SpecType)]
xts = [(Id
x, Template SpecType
to) | (Id
x, CoreExpr
_, Template SpecType
to) <- [(Id, CoreExpr, Template SpecType)]
xets]
CGEnv
γ' <- (CGEnv -> (Id, Template SpecType) -> CG CGEnv)
-> CGEnv -> [(Id, Template SpecType)] -> CG CGEnv
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM CGEnv -> (Id, Template SpecType) -> CG CGEnv
forall a. Symbolic a => CGEnv -> (a, Template SpecType) -> CG CGEnv
extender (CGEnv
γ CGEnv -> [Id] -> CGEnv
`setRecs` ((Id, Template SpecType) -> Id
forall a b. (a, b) -> a
fst ((Id, Template SpecType) -> Id)
-> [(Id, Template SpecType)] -> [Id]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Id, Template SpecType)]
xts)) [(Id, Template SpecType)]
xts
((Id, CoreExpr, Template SpecType) -> CG (Template SpecType))
-> [(Id, CoreExpr, Template SpecType)] -> State CGInfo ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Bool
-> CGEnv
-> (Id, CoreExpr, Template SpecType)
-> CG (Template SpecType)
consBind Bool
True CGEnv
γ') [(Id, CoreExpr, Template SpecType)]
xets
CGEnv -> CG CGEnv
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return CGEnv
γ'
consCB TCheck
NoCheck CGEnv
γ (Rec [(Id, CoreExpr)]
xes)
= do [(Id, CoreExpr, Template SpecType)]
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))
(CGInfo -> CGInfo) -> State CGInfo ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((CGInfo -> CGInfo) -> State CGInfo ())
-> (CGInfo -> CGInfo) -> State CGInfo ()
forall a b. (a -> b) -> a -> b
$ \CGInfo
i -> CGInfo
i { recCount = recCount i + length xes }
let xts :: [(Id, Template SpecType)]
xts = [(Id
x, Template SpecType
to) | (Id
x, CoreExpr
_, Template SpecType
to) <- [(Id, CoreExpr, Template SpecType)]
xets]
CGEnv
γ' <- (CGEnv -> (Id, Template SpecType) -> CG CGEnv)
-> CGEnv -> [(Id, Template SpecType)] -> CG CGEnv
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM CGEnv -> (Id, Template SpecType) -> CG CGEnv
forall a. Symbolic a => CGEnv -> (a, Template SpecType) -> CG CGEnv
extender (CGEnv
γ CGEnv -> [Id] -> CGEnv
`setRecs` ((Id, Template SpecType) -> Id
forall a b. (a, b) -> a
fst ((Id, Template SpecType) -> Id)
-> [(Id, Template SpecType)] -> [Id]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Id, Template SpecType)]
xts)) [(Id, Template SpecType)]
xts
((Id, CoreExpr, Template SpecType) -> CG (Template SpecType))
-> [(Id, CoreExpr, Template SpecType)] -> State CGInfo ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Bool
-> CGEnv
-> (Id, CoreExpr, Template SpecType)
-> CG (Template SpecType)
consBind Bool
True CGEnv
γ') [(Id, CoreExpr, Template SpecType)]
xets
CGEnv -> CG CGEnv
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return CGEnv
γ'
consCB TCheck
_ CGEnv
γ (NonRec Id
x CoreExpr
_) | Id -> Bool
isDictionary Id
x
= do SpecType
t <- Bool -> Type -> CG SpecType
trueTy (Config -> Bool
typeclass (CGEnv -> Config
forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)) (Id -> Type
varType Id
x)
CGEnv -> (Id, Template SpecType) -> CG CGEnv
forall a. Symbolic a => CGEnv -> (a, Template SpecType) -> CG CGEnv
extender CGEnv
γ (Id
x, SpecType -> Template SpecType
forall a. a -> Template a
Assumed SpecType
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 [SpecType]
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]
τ
(WfC -> State CGInfo ()) -> [WfC] -> State CGInfo ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ WfC -> State CGInfo ()
addW (CGEnv -> SpecType -> WfC
WfC CGEnv
γ (SpecType -> WfC) -> [SpecType] -> [WfC]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SpecType]
st)
let xts :: HashMap Symbol (RISig SpecType)
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
γ' = CGEnv
γ { denv = dinsert (denv γ) x xts }
SpecType
t <- Bool -> Type -> CG SpecType
trueTy (Config -> Bool
typeclass (CGEnv -> Config
forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)) (Id -> Type
varType Id
x)
CGEnv -> (Id, Template SpecType) -> CG CGEnv
forall a. Symbolic a => CGEnv -> (a, Template SpecType) -> CG CGEnv
extender CGEnv
γ' (Id
x, SpecType -> Template SpecType
forall a. a -> Template a
Assumed SpecType
t)
where
f :: [RType c tv r] -> RType c tv r -> RType c tv r
f [RType c tv r
t'] (RAllT RTVar tv (RType c tv ())
α RType c tv r
te r
_) = (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 Template SpecType
to <- CGEnv -> (Id, Maybe CoreExpr) -> CG (Template SpecType)
varTemplate CGEnv
γ (Id
x, Maybe CoreExpr
forall a. Maybe a
Nothing)
Template SpecType
to' <- Bool
-> CGEnv
-> (Id, CoreExpr, Template SpecType)
-> CG (Template SpecType)
consBind Bool
False CGEnv
γ (Id
x, CoreExpr
e, Template SpecType
to) CG (Template SpecType)
-> (Template SpecType -> CG (Template SpecType))
-> CG (Template SpecType)
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
>>= CGEnv -> Template SpecType -> CG (Template SpecType)
addPostTemplate CGEnv
γ
CGEnv -> (Id, Template SpecType) -> CG CGEnv
forall a. Symbolic a => CGEnv -> (a, Template SpecType) -> CG CGEnv
extender CGEnv
γ (Id
x, CGEnv -> CoreExpr -> SpecType -> SpecType
makeSingleton CGEnv
γ (CoreExpr -> CoreExpr
simplify CoreExpr
e) (SpecType -> SpecType) -> Template SpecType -> Template SpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Template SpecType
to')
grepDictionary :: CoreExpr -> Maybe (Var, [Type])
grepDictionary :: CoreExpr -> Maybe (Id, [Type])
grepDictionary = [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
= 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)]
_,[PVar (RType RTyCon RTyVar ())]
πs,SpecType
_) = SpecType
-> ([(RTVar RTyVar (RType RTyCon RTyVar ()), RReft)],
[PVar (RType RTyCon RTyVar ())], SpecType)
forall tv c r.
RType tv c r
-> ([(RTVar c (RType tv c ()), r)], [PVar (RType tv c ())],
RType tv c r)
bkUniv SpecType
spect
CGEnv
cgenv <- (CGEnv -> PVar (RType RTyCon RTyVar ()) -> CG CGEnv)
-> CGEnv -> [PVar (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 -> PVar (RType RTyCon RTyVar ()) -> CG CGEnv
addPToEnv CGEnv
γ' [PVar (RType RTyCon RTyVar ())]
πs
CGEnv -> CoreExpr -> SpecType -> State CGInfo ()
cconsE CGEnv
cgenv CoreExpr
e (Bool -> Id -> SpecType -> SpecType
weakenResult (Config -> Bool
typeclass (CGEnv -> Config
forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)) Id
x SpecType
spect)
Bool -> State CGInfo () -> State CGInfo ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Id -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Id
x Symbol -> HEnv -> Bool
`elemHEnv` CGEnv -> HEnv
holes CGEnv
γ) (State CGInfo () -> State CGInfo ())
-> State CGInfo () -> State CGInfo ()
forall a b. (a -> b) -> a -> b
$
WfC -> State CGInfo ()
addW (WfC -> State CGInfo ()) -> WfC -> State CGInfo ()
forall a b. (a -> b) -> a -> b
$ CGEnv -> SpecType -> WfC
WfC CGEnv
cgenv (SpecType -> WfC) -> SpecType -> WfC
forall a b. (a -> b) -> a -> b
$ (RReft -> RReft) -> SpecType -> SpecType
forall a b.
(a -> b) -> RType RTyCon RTyVar a -> RType RTyCon RTyVar b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap RReft -> RReft
killSubst SpecType
spect
Id -> Annot SpecType -> State CGInfo ()
addIdA Id
x (Bool -> SpecType -> Annot SpecType
forall t. Bool -> t -> Annot t
defAnn Bool
isRec' SpecType
spect)
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
$ SpecType -> Template SpecType
forall a. a -> Template a
Asserted SpecType
spect
consBind Bool
isRec' CGEnv
γ (Id
x, CoreExpr
e, Internal SpecType
spect)
= do let γ' :: CGEnv
γ' = CGEnv
γ CGEnv -> Id -> CGEnv
`setBind` Id
x
([(RTVar RTyVar (RType RTyCon RTyVar ()), RReft)]
_,[PVar (RType RTyCon RTyVar ())]
πs,SpecType
_) = SpecType
-> ([(RTVar RTyVar (RType RTyCon RTyVar ()), RReft)],
[PVar (RType RTyCon RTyVar ())], SpecType)
forall tv c r.
RType tv c r
-> ([(RTVar c (RType tv c ()), r)], [PVar (RType tv c ())],
RType tv c r)
bkUniv SpecType
spect
CGEnv
γπ <- (CGEnv -> PVar (RType RTyCon RTyVar ()) -> CG CGEnv)
-> CGEnv -> [PVar (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 -> PVar (RType RTyCon RTyVar ()) -> CG CGEnv
addPToEnv CGEnv
γ' [PVar (RType RTyCon RTyVar ())]
πs
let γπ' :: CGEnv
γπ' = CGEnv
γπ {cerr = Just $ ErrHMeas (getLocation γπ) (pprint x) (text explanation)}
CGEnv -> CoreExpr -> SpecType -> State CGInfo ()
cconsE CGEnv
γπ' CoreExpr
e SpecType
spect
Bool -> State CGInfo () -> State CGInfo ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Id -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Id
x Symbol -> HEnv -> Bool
`elemHEnv` CGEnv -> HEnv
holes CGEnv
γ) (State CGInfo () -> State CGInfo ())
-> State CGInfo () -> State CGInfo ()
forall a b. (a -> b) -> a -> b
$
WfC -> State CGInfo ()
addW (WfC -> State CGInfo ()) -> WfC -> State CGInfo ()
forall a b. (a -> b) -> a -> b
$ CGEnv -> SpecType -> WfC
WfC CGEnv
γπ (SpecType -> WfC) -> SpecType -> WfC
forall a b. (a -> b) -> a -> b
$ (RReft -> RReft) -> SpecType -> SpecType
forall a b.
(a -> b) -> RType RTyCon RTyVar a -> RType RTyCon RTyVar b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap RReft -> RReft
killSubst SpecType
spect
Id -> Annot SpecType -> State CGInfo ()
addIdA Id
x (Bool -> SpecType -> Annot SpecType
forall t. Bool -> t -> Annot t
defAnn Bool
isRec' SpecType
spect)
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
$ SpecType -> Template SpecType
forall a. a -> Template a
Internal SpecType
spect
where
explanation :: a
explanation = a
"Cannot give singleton type to the function definition."
consBind Bool
isRec' CGEnv
γ (Id
x, CoreExpr
e, Assumed SpecType
spect)
= do let γ' :: CGEnv
γ' = CGEnv
γ CGEnv -> Id -> CGEnv
`setBind` Id
x
CGEnv
γπ <- (CGEnv -> PVar (RType RTyCon RTyVar ()) -> CG CGEnv)
-> CGEnv -> [PVar (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 -> PVar (RType RTyCon RTyVar ()) -> CG CGEnv
addPToEnv CGEnv
γ' [PVar (RType RTyCon RTyVar ())]
πs
CGEnv -> CoreExpr -> SpecType -> State CGInfo ()
cconsE CGEnv
γπ CoreExpr
e (SpecType -> State CGInfo ()) -> CG SpecType -> State CGInfo ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< 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
spect
Id -> Annot SpecType -> State CGInfo ()
addIdA Id
x (Bool -> SpecType -> Annot SpecType
forall t. Bool -> t -> Annot t
defAnn Bool
isRec' SpecType
spect)
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
$ SpecType -> Template SpecType
forall a. a -> Template a
Asserted SpecType
spect
where πs :: [PVar (RType RTyCon RTyVar ())]
πs = RTypeRep RTyCon RTyVar RReft -> [PVar (RType RTyCon RTyVar ())]
forall c tv r. RTypeRep c tv r -> [PVar (RType c tv ())]
ty_preds (RTypeRep RTyCon RTyVar RReft -> [PVar (RType RTyCon RTyVar ())])
-> RTypeRep RTyCon RTyVar RReft -> [PVar (RType RTyCon RTyVar ())]
forall a b. (a -> b) -> a -> b
$ SpecType -> RTypeRep RTyCon RTyVar RReft
forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep SpecType
spect
consBind Bool
isRec' CGEnv
γ (Id
x, CoreExpr
e, Template SpecType
Unknown)
= do SpecType
t' <- CGEnv -> CoreExpr -> CG SpecType
consE (CGEnv
γ CGEnv -> Id -> CGEnv
`setBind` Id
x) CoreExpr
e
SpecType
t <- Id -> SpecType -> CG SpecType
topSpecType Id
x SpecType
t'
Id -> Annot SpecType -> State CGInfo ()
addIdA Id
x (Bool -> SpecType -> Annot SpecType
forall t. Bool -> t -> Annot t
defAnn Bool
isRec' SpecType
t)
Bool -> State CGInfo () -> State CGInfo ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Id -> Bool
GM.isExternalId Id
x) (Id -> SpecType -> State CGInfo ()
forall a. PPrint a => a -> SpecType -> State CGInfo ()
addKuts Id
x SpecType
t)
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
$ SpecType -> Template SpecType
forall a. a -> Template a
Asserted SpecType
t
killSubst :: RReft -> RReft
killSubst :: RReft -> RReft
killSubst = (Reft -> Reft) -> RReft -> RReft
forall a b. (a -> b) -> UReft a -> UReft 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 = Visitor () () -> () -> () -> Reft -> Reft
forall t a ctx.
(Visitable t, Monoid a) =>
Visitor a ctx -> ctx -> a -> t -> t
trans Visitor () ()
forall {acc} {ctx}. Monoid acc => Visitor acc ctx
kv () ()
where
kv :: Visitor acc ctx
kv = Visitor acc ctx
forall {acc} {ctx}. Monoid acc => Visitor acc ctx
defaultVisitor { txExpr = ks }
ks :: p -> Expr -> Expr
ks p
_ (F.PKVar KVar
k Subst
_) = KVar -> Subst -> Expr
F.PKVar KVar
k Subst
forall a. Monoid a => a
mempty
ks p
_ Expr
p = Expr
p
defAnn :: Bool -> t -> Annot t
defAnn :: forall t. Bool -> t -> Annot t
defAnn Bool
True = 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 -> PVar (RType RTyCon RTyVar ()) -> CG CGEnv
addPToEnv CGEnv
γ PVar (RType RTyCon RTyVar ())
π
= do CGEnv
γπ <- CGEnv
γ CGEnv -> ([Char], Symbol, SpecType) -> CG CGEnv
+= ([Char]
"addSpec1", PVar (RType RTyCon RTyVar ()) -> Symbol
forall t. PVar t -> Symbol
pname PVar (RType RTyCon RTyVar ())
π, PVar (RType RTyCon RTyVar ()) -> SpecType
forall r.
(PPrint r, Reftable r) =>
PVar (RType RTyCon RTyVar ()) -> RRType r
pvarRType PVar (RType RTyCon RTyVar ())
π)
(CGEnv -> ([Char], Symbol, SpecType) -> CG CGEnv)
-> CGEnv -> [([Char], Symbol, SpecType)] -> CG CGEnv
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM CGEnv -> ([Char], Symbol, SpecType) -> CG CGEnv
(+=) CGEnv
γπ [([Char]
"addSpec2", Symbol
x, RType RTyCon RTyVar () -> SpecType
forall r c tv. Reftable r => RType c tv () -> RType c tv r
ofRSort RType RTyCon RTyVar ()
t) | (RType RTyCon RTyVar ()
t, Symbol
x, Expr
_) <- PVar (RType RTyCon RTyVar ())
-> [(RType RTyCon RTyVar (), Symbol, Expr)]
forall t. PVar t -> [(t, Symbol, Expr)]
pargs PVar (RType RTyCon RTyVar ())
π]
cconsE :: CGEnv -> CoreExpr -> SpecType -> CG ()
cconsE :: CGEnv -> CoreExpr -> SpecType -> State CGInfo ()
cconsE CGEnv
g CoreExpr
e SpecType
t = do
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 HashSet Id
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 Id
x Id -> HashSet Id -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`S.member` HashSet Id
sp
then CGEnv -> CoreExpr -> SpecType -> State CGInfo ()
cconsLazyLet CGEnv
γ CoreExpr
e SpecType
t
else do CGEnv
γ' <- CGEnv -> CoreBind -> CG CGEnv
consCBLet CGEnv
γ CoreBind
b
CGEnv -> CoreExpr -> SpecType -> State CGInfo ()
cconsE CGEnv
γ' CoreExpr
ee SpecType
t
cconsE' CGEnv
γ CoreExpr
e (RAllP PVar (RType RTyCon RTyVar ())
p SpecType
t)
= CGEnv -> CoreExpr -> SpecType -> State CGInfo ()
cconsE CGEnv
γ' CoreExpr
e SpecType
t''
where
t' :: SpecType
t' = (UsedPVar, (Symbol, [((), Symbol, Expr)]) -> Expr)
-> RReft -> RReft
replacePredsWithRefs (UsedPVar, (Symbol, [((), Symbol, Expr)]) -> Expr)
forall {a} {b}. (UsedPVar, (Symbol, [(a, b, Expr)]) -> Expr)
su (RReft -> RReft) -> SpecType -> SpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SpecType
t
su :: (UsedPVar, (Symbol, [(a, b, Expr)]) -> Expr)
su = (PVar (RType RTyCon RTyVar ()) -> UsedPVar
forall t. PVar t -> UsedPVar
uPVar PVar (RType RTyCon RTyVar ())
p, PVar (RType RTyCon RTyVar ()) -> (Symbol, [(a, b, Expr)]) -> Expr
forall t a b. PVar t -> (Symbol, [(a, b, Expr)]) -> Expr
pVartoRConc PVar (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
γ' <- CGEnv -> CoreBind -> CG CGEnv
consCBLet CGEnv
γ CoreBind
b
CGEnv -> CoreExpr -> SpecType -> State CGInfo ()
cconsE CGEnv
γ' CoreExpr
e SpecType
t
cconsE' CGEnv
γ (Case CoreExpr
e Id
x Type
_ [Alt Id]
cases) SpecType
t
= do CGEnv
γ' <- CGEnv -> CoreBind -> CG CGEnv
consCBLet CGEnv
γ (Id -> CoreExpr -> CoreBind
forall b. b -> Expr b -> Bind b
NonRec Id
x CoreExpr
e)
[Alt Id] -> (Alt Id -> State CGInfo ()) -> State CGInfo ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Alt Id]
cases ((Alt Id -> State CGInfo ()) -> State CGInfo ())
-> (Alt Id -> State CGInfo ()) -> State CGInfo ()
forall a b. (a -> b) -> a -> b
$ CGEnv -> Id -> SpecType -> [AltCon] -> Alt Id -> State CGInfo ()
cconsCase CGEnv
γ' Id
x SpecType
t [AltCon]
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
γ' <- CGEnv -> Id -> CG CGEnv
updateEnvironment CGEnv
γ Id
α
CGEnv -> Id -> CoreExpr -> SpecType -> State CGInfo ()
addForAllConstraint CGEnv
γ' Id
α CoreExpr
e (RTVar RTyVar (RType RTyCon RTyVar ())
-> SpecType -> RReft -> SpecType
forall c tv r. RTVU c tv -> RType c tv r -> r -> RType c tv r
RAllT RTVar RTyVar (RType RTyCon RTyVar ())
α' SpecType
t RReft
r)
CGEnv -> CoreExpr -> SpecType -> State CGInfo ()
cconsE CGEnv
γ' CoreExpr
e (SpecType -> State CGInfo ()) -> SpecType -> State CGInfo ()
forall a b. (a -> b) -> a -> b
$ (RTyVar, SpecType) -> SpecType -> SpecType
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 RTyVar (RType RTyCon RTyVar ()) -> RTyVar
forall tv s. RTVar tv s -> tv
ty_var_value RTVar RTyVar (RType RTyCon RTyVar ())
α', Id -> SpecType
forall r c. Monoid r => Id -> RType c RTyVar r
rVar Id
α) SpecType
t
cconsE' CGEnv
γ (Lam Id
x CoreExpr
e) (RFun Symbol
y RFInfo
i SpecType
ty SpecType
t RReft
r)
| Bool -> Bool
not (Id -> Bool
isTyVar Id
x)
= do CGEnv
γ' <- CGEnv
γ CGEnv -> ([Char], Symbol, SpecType) -> CG CGEnv
+= ([Char]
"cconsE", Symbol
x', SpecType
ty)
CGEnv -> CoreExpr -> SpecType -> State CGInfo ()
cconsE CGEnv
γ' CoreExpr
e SpecType
t'
CGEnv -> Id -> CoreExpr -> SpecType -> State CGInfo ()
addFunctionConstraint CGEnv
γ Id
x CoreExpr
e (Symbol -> RFInfo -> SpecType -> SpecType -> RReft -> SpecType
forall c tv r.
Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
x' RFInfo
i SpecType
ty SpecType
t' RReft
r')
Id -> Annot SpecType -> State CGInfo ()
addIdA Id
x (SpecType -> Annot SpecType
forall t. t -> Annot t
AnnDef SpecType
ty)
where
x' :: Symbol
x' = Id -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Id
x
t' :: SpecType
t' = SpecType
t SpecType -> (Symbol, Expr) -> SpecType
forall a. Subable a => a -> (Symbol, Expr) -> a
`F.subst1` (Symbol
y, Symbol -> Expr
F.EVar Symbol
x')
r' :: RReft
r' = RReft
r RReft -> (Symbol, Expr) -> RReft
forall a. Subable a => a -> (Symbol, Expr) -> a
`F.subst1` (Symbol
y, Symbol -> Expr
F.EVar Symbol
x')
cconsE' CGEnv
γ (Tick CoreTickish
tt CoreExpr
e) SpecType
t
= CGEnv -> CoreExpr -> SpecType -> 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
| 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 SpecType
t' <- CGEnv -> Type -> CoreExpr -> CoercionR -> CG SpecType
castTy CGEnv
γ ((() :: Constraint) => CoreExpr -> Type
CoreExpr -> Type
exprType CoreExpr
e) CoreExpr
e' CoercionR
c
SubC -> [Char] -> State CGInfo ()
addC (CGEnv -> SpecType -> SpecType -> SubC
SubC CGEnv
γ ([Char] -> SpecType -> SpecType
forall a. PPrint a => [Char] -> a -> a
F.notracepp ([Char]
"Casted Type for " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ CoreExpr -> [Char]
forall a. Outputable a => a -> [Char]
GM.showPpr CoreExpr
e [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n init type " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SpecType -> [Char]
forall a. PPrint a => a -> [Char]
showpp SpecType
t) SpecType
t') SpecType
t) ([Char]
"cconsE Cast: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ CoreExpr -> [Char]
forall a. Outputable a => a -> [Char]
GM.showPpr CoreExpr
e)
cconsE' CGEnv
γ CoreExpr
e SpecType
t
= do SpecType
te <- CGEnv -> CoreExpr -> CG SpecType
consE CGEnv
γ CoreExpr
e
SpecType
te' <- CGEnv -> CoreExpr -> SpecType -> CG SpecType
instantiatePreds CGEnv
γ CoreExpr
e SpecType
te CG SpecType -> (SpecType -> CG SpecType) -> CG SpecType
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
>>= CGEnv -> SpecType -> CG SpecType
addPost CGEnv
γ
SubC -> [Char] -> State CGInfo ()
addC (CGEnv -> SpecType -> SpecType -> SubC
SubC CGEnv
γ SpecType
te' SpecType
t) ([Char]
"cconsE: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n t = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SpecType -> [Char]
forall a. PPrint a => a -> [Char]
showpp SpecType
t [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n te = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SpecType -> [Char]
forall a. PPrint a => a -> [Char]
showpp SpecType
te [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ CoreExpr -> [Char]
forall a. Outputable a => a -> [Char]
GM.showPpr CoreExpr
e)
lambdaSingleton :: CGEnv -> F.TCEmb TyCon -> Var -> CoreExpr -> CG (UReft F.Reft)
lambdaSingleton :: CGEnv -> TCEmb TyCon -> Id -> CoreExpr -> CG RReft
lambdaSingleton CGEnv
γ TCEmb TyCon
tce Id
x CoreExpr
e
| CGEnv -> Bool
forall t. HasConfig t => t -> Bool
higherOrderFlag CGEnv
γ
= do Maybe Expr
expr <- CGEnv -> CoreExpr -> CG (Maybe Expr)
lamExpr CGEnv
γ CoreExpr
e
RReft -> CG RReft
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (RReft -> CG RReft) -> RReft -> CG RReft
forall a b. (a -> b) -> a -> b
$ case Maybe Expr
expr of
Just Expr
e' -> Reft -> RReft
forall r. r -> UReft r
uTop (Reft -> RReft) -> Reft -> RReft
forall a b. (a -> b) -> a -> b
$ Expr -> Reft
forall a. Expression a => a -> Reft
F.exprReft (Expr -> Reft) -> Expr -> Reft
forall a b. (a -> b) -> a -> b
$ (Symbol, Sort) -> Expr -> Expr
F.ELam (Id -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Id
x, Sort
sx) Expr
e'
Maybe Expr
_ -> 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
F.isTauto RReft
rr
= () -> State CGInfo ()
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
| Bool
otherwise
= do SpecType
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 :: RReft -> SpecType
truet = RTVar RTyVar (RType RTyCon RTyVar ())
-> SpecType -> RReft -> SpecType
forall c tv r. RTVU c tv -> RType c tv r -> r -> RType 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 {c} {tv} {r}. RType c tv r -> RType c tv r
unRAllP SpecType
t'
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
rr) [Char]
"forall constraint true"
where unRAllP :: RType c tv r -> RType c tv r
unRAllP (RAllT RTVU c tv
a RType c tv r
t r
r) = RTVU c tv -> RType c tv r -> r -> RType c tv r
forall c tv r. RTVU c tv -> RType c tv r -> r -> RType c tv r
RAllT RTVU c tv
a (RType c tv r -> RType c tv r
unRAllP RType c tv r
t) r
r
unRAllP (RAllP PVU c tv
_ RType c tv r
t) = RType c tv r -> RType c tv r
unRAllP RType c tv r
t
unRAllP RType c tv r
t = RType c tv r
t
addForAllConstraint CGEnv
γ Id
_ CoreExpr
_ SpecType
_
= 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 SpecType
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
SpecType
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
t
let truet :: RReft -> SpecType
truet = Symbol -> RFInfo -> SpecType -> SpecType -> RReft -> SpecType
forall c tv r.
Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
y RFInfo
i SpecType
ty' SpecType
t'
Maybe Expr
lamE <- CGEnv -> CoreExpr -> CG (Maybe Expr)
lamExpr CGEnv
γ CoreExpr
e
case (Maybe Expr
lamE, CGEnv -> Bool
forall t. HasConfig t => t -> Bool
higherOrderFlag CGEnv
γ) of
(Just Expr
e', Bool
True) -> do TCEmb TyCon
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 :: Sort
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 :: RReft
ref = Reft -> RReft
forall r. r -> UReft r
uTop (Reft -> RReft) -> Reft -> RReft
forall a b. (a -> b) -> a -> b
$ Expr -> Reft
forall a. Expression a => a -> Reft
F.exprReft (Expr -> Reft) -> Expr -> Reft
forall a b. (a -> b) -> a -> b
$ (Symbol, Sort) -> Expr -> Expr
F.ELam (Id -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Id
x, Sort
sx) Expr
e'
SubC -> [Char] -> State CGInfo ()
addC (CGEnv -> SpecType -> SpecType -> SubC
SubC CGEnv
γ (RReft -> SpecType
truet RReft
ref) (SpecType -> SubC) -> SpecType -> SubC
forall a b. (a -> b) -> a -> b
$ RReft -> SpecType
truet RReft
r) [Char]
"function constraint singleton"
(Maybe Expr, 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, RType c tv r)]
cs r
_ Oblig
OCons RType c tv r
t)
= let ([[(Symbol, RType c tv r)]]
css, RType c tv r
t') = Bool -> RType c tv r -> ([[(Symbol, RType c tv r)]], RType 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 RType c tv r
t in ([(Symbol, RType c tv r)]
cs[(Symbol, RType c tv r)]
-> [[(Symbol, RType c tv r)]] -> [[(Symbol, RType c tv r)]]
forall a. a -> [a] -> [a]
:[[(Symbol, RType c tv r)]]
css, RType c tv r
t')
splitConstraints Bool
allowTC (RFun Symbol
x RFInfo
i tx :: RType c tv r
tx@(RApp c
c [RType c tv r]
_ [RTProp c tv r]
_ r
_) RType c tv r
t r
r) | c -> Bool
forall {c}. TyConable c => c -> Bool
isErasable c
c
= let ([[(Symbol, RType c tv r)]]
css, RType c tv r
t') = Bool -> RType c tv r -> ([[(Symbol, RType c tv r)]], RType 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 RType c tv r
t in ([[(Symbol, RType c tv r)]]
css, Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
forall c tv r.
Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
x RFInfo
i RType c tv r
tx RType c tv r
t' r
r)
where isErasable :: c -> Bool
isErasable = if Bool
allowTC then c -> Bool
forall {c}. TyConable c => c -> Bool
isEmbeddedDict else c -> Bool
forall {c}. TyConable c => c -> Bool
isClass
splitConstraints Bool
_ RType c tv r
t
= ([], RType c tv r
t)
instantiatePreds :: CGEnv
-> CoreExpr
-> SpecType
-> CG SpecType
instantiatePreds :: CGEnv -> CoreExpr -> SpecType -> CG SpecType
instantiatePreds CGEnv
γ CoreExpr
e (RAllP PVar (RType RTyCon RTyVar ())
π SpecType
t)
= do RTProp RTyCon RTyVar RReft
r <- CGEnv
-> CoreExpr
-> PVar (RType RTyCon RTyVar ())
-> CG (RTProp RTyCon RTyVar RReft)
freshPredRef CGEnv
γ CoreExpr
e PVar (RType RTyCon RTyVar ())
π
CGEnv -> CoreExpr -> SpecType -> CG SpecType
instantiatePreds CGEnv
γ CoreExpr
e (SpecType -> CG SpecType) -> SpecType -> CG SpecType
forall a b. (a -> b) -> a -> b
$ [Char]
-> SpecType
-> [(PVar (RType RTyCon RTyVar ()), RTProp RTyCon RTyVar RReft)]
-> SpecType
replacePreds [Char]
"consE" SpecType
t [(PVar (RType RTyCon RTyVar ())
π, RTProp RTyCon RTyVar RReft
r)]
instantiatePreds CGEnv
_ CoreExpr
_ SpecType
t0
= 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 SpecType
tx <- Bool -> Type -> CG SpecType
trueTy (Config -> Bool
typeclass (CGEnv -> Config
forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)) (Id -> Type
varType Id
x)
CGEnv
γ' <- (CGEnv
γ, [Char]
"Let NonRec") (CGEnv, [Char]) -> (Symbol, CoreExpr, SpecType) -> CG CGEnv
+++= (Id -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Id
x, CoreExpr
ex, SpecType
tx)
CGEnv -> CoreExpr -> SpecType -> State CGInfo ()
cconsE CGEnv
γ' CoreExpr
e SpecType
t
cconsLazyLet CGEnv
_ CoreExpr
_ SpecType
_
= Maybe SrcSpan -> [Char] -> State CGInfo ()
forall a. Maybe SrcSpan -> [Char] -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing [Char]
"Constraint.Generate.cconsLazyLet called on invalid inputs"
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) ((() :: Constraint) => CoreExpr -> Type
CoreExpr -> Type
exprType CoreExpr
e)
consE CGEnv
γ (Var Id
x) | Id -> Bool
GM.isDataConId Id
x
= do SpecType
t0 <- (?callStack::CallStack) => CGEnv -> Id -> CG SpecType
CGEnv -> Id -> CG SpecType
varRefType CGEnv
γ Id
x
let hasSelf :: Bool
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 :: SpecType
t = if Bool
hasSelf
then (Reft -> Reft) -> RReft -> RReft
forall a b. (a -> b) -> UReft a -> UReft 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
Maybe Id -> SrcSpan -> Annot SpecType -> State CGInfo ()
addLocA (Id -> Maybe Id
forall a. a -> Maybe a
Just Id
x) (CGEnv -> SrcSpan
getLocation CGEnv
γ) (CGEnv -> Id -> SpecType -> Annot SpecType
forall t. CGEnv -> Id -> t -> Annot t
varAnn CGEnv
γ Id
x SpecType
t)
SpecType -> CG SpecType
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return SpecType
t
consE CGEnv
γ (Var Id
x)
= do SpecType
t <- (?callStack::CallStack) => CGEnv -> Id -> CG SpecType
CGEnv -> Id -> CG SpecType
varRefType CGEnv
γ Id
x
Maybe Id -> SrcSpan -> Annot SpecType -> State CGInfo ()
addLocA (Id -> Maybe Id
forall a. a -> Maybe a
Just Id
x) (CGEnv -> SrcSpan
getLocation CGEnv
γ) (CGEnv -> Id -> SpecType -> Annot SpecType
forall t. CGEnv -> Id -> t -> Annot t
varAnn CGEnv
γ Id
x SpecType
t)
SpecType -> CG SpecType
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return SpecType
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 RTVar RTyVar (RType RTyCon RTyVar ())
α SpecType
te RReft
_ <- ([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
SpecType
t <- if Bool -> Bool
not (Config -> Bool
nopolyinfer (CGEnv -> Config
forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)) Bool -> Bool -> Bool
&& RTVar RTyVar (RType RTyCon RTyVar ()) -> Bool
forall {tv} {s}. RTVar tv s -> Bool
isPos RTVar RTyVar (RType RTyCon RTyVar ())
α Bool -> Bool -> Bool
&& RTyVar -> SpecType -> Bool
isGenericVar (RTVar RTyVar (RType RTyCon RTyVar ()) -> RTyVar
forall tv s. RTVar tv s -> tv
ty_var_value RTVar RTyVar (RType RTyCon RTyVar ())
α) SpecType
te
then Bool -> KVKind -> CoreExpr -> Type -> CG SpecType
freshTyType (Config -> Bool
typeclass (CGEnv -> Config
forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)) KVKind
TypeInstE CoreExpr
e Type
τ
else Bool -> Type -> CG SpecType
trueTy (Config -> Bool
typeclass (CGEnv -> Config
forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)) Type
τ
WfC -> State CGInfo ()
addW (WfC -> State CGInfo ()) -> WfC -> State CGInfo ()
forall a b. (a -> b) -> a -> b
$ CGEnv -> SpecType -> WfC
WfC CGEnv
γ SpecType
t
SpecType
t' <- SpecType -> CG SpecType
forall (m :: * -> *). FreshM m => SpecType -> m SpecType
refreshVV SpecType
t
SpecType
tt0 <- CGEnv -> CoreExpr -> SpecType -> CG SpecType
instantiatePreds CGEnv
γ CoreExpr
e' ((RTyVar, SpecType) -> SpecType -> SpecType
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 RTyVar (RType RTyCon RTyVar ()) -> RTyVar
forall tv s. RTVar tv s -> tv
ty_var_value RTVar RTyVar (RType RTyCon RTyVar ())
α, SpecType
t') SpecType
te)
let tt :: SpecType
tt = CGEnv -> CoreExpr -> SpecType -> SpecType
makeSingleton CGEnv
γ (CoreExpr -> CoreExpr
simplify CoreExpr
e') (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
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
$ case RTVar RTyVar (RType RTyCon RTyVar ())
-> Maybe (Symbol, RType RTyCon RTyVar ())
forall s. RTVar RTyVar s -> Maybe (Symbol, s)
rTVarToBind RTVar RTyVar (RType RTyCon RTyVar ())
α of
Just (Symbol
x, RType RTyCon RTyVar ()
_) -> SpecType -> (Expr -> SpecType) -> Maybe Expr -> 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, Expr) -> SpecType
forall a. Subable a => a -> (Symbol, Expr) -> a
F.subst1 SpecType
tt ((Symbol, Expr) -> SpecType)
-> (Expr -> (Symbol, Expr)) -> Expr -> SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol
x,)) (Type -> Maybe Expr
argType Type
τ)
Maybe (Symbol, RType RTyCon RTyVar ())
Nothing -> SpecType
tt
where
isPos :: RTVar tv s -> Bool
isPos RTVar tv s
α = Bool -> Bool
not (Config -> Bool
extensionality (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
([], [PVar (RType RTyCon RTyVar ())]
πs, SpecType
te) <- SpecType
-> ([(RTVar RTyVar (RType RTyCon RTyVar ()), RReft)],
[PVar (RType RTyCon RTyVar ())], SpecType)
forall tv c r.
RType tv c r
-> ([(RTVar c (RType tv c ()), r)], [PVar (RType tv c ())],
RType tv c r)
bkUniv (SpecType
-> ([(RTVar RTyVar (RType RTyCon RTyVar ()), RReft)],
[PVar (RType RTyCon RTyVar ())], SpecType))
-> CG SpecType
-> StateT
CGInfo
Identity
([(RTVar RTyVar (RType RTyCon RTyVar ()), RReft)],
[PVar (RType RTyCon RTyVar ())], SpecType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CGEnv -> CoreExpr -> CG SpecType
consE CGEnv
γ CoreExpr
e
SpecType
te' <- CGEnv -> CoreExpr -> SpecType -> CG SpecType
instantiatePreds CGEnv
γ CoreExpr
e' (SpecType -> CG SpecType) -> SpecType -> CG SpecType
forall a b. (a -> b) -> a -> b
$ (PVar (RType RTyCon RTyVar ()) -> SpecType -> SpecType)
-> SpecType -> [PVar (RType RTyCon RTyVar ())] -> SpecType
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr PVar (RType RTyCon RTyVar ()) -> SpecType -> SpecType
forall c tv r. PVU c tv -> RType c tv r -> RType c tv r
RAllP SpecType
te [PVar (RType RTyCon RTyVar ())]
πs
(CGEnv
γ', SpecType
te''') <- CGEnv -> SpecType -> CG (CGEnv, SpecType)
dropExists CGEnv
γ SpecType
te'
SpecType
te'' <- CGEnv -> SpecType -> CG SpecType
dropConstraints CGEnv
γ SpecType
te'''
Maybe SrcSpan -> SpecType -> State CGInfo ()
updateLocA (CoreExpr -> Maybe SrcSpan
exprLoc CoreExpr
e) SpecType
te''
let RFun Symbol
x RFInfo
_ SpecType
tx SpecType
t RReft
_ = ([Char], CoreExpr) -> CGEnv -> SpecType -> SpecType
forall a.
Outputable a =>
([Char], a) -> CGEnv -> SpecType -> SpecType
checkFun ([Char]
"Non-fun App with caller ", CoreExpr
e') CGEnv
γ SpecType
te''
CGEnv -> CoreExpr -> SpecType -> State CGInfo ()
cconsE CGEnv
γ' CoreExpr
a SpecType
tx
CGEnv -> SpecType -> CG SpecType
addPost CGEnv
γ' (SpecType -> CG SpecType) -> SpecType -> CG SpecType
forall a b. (a -> b) -> a -> b
$ SpecType -> (Expr -> SpecType) -> Maybe Expr -> 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
t CoreExpr
a) (SpecType -> (Symbol, Expr) -> SpecType
forall a. Subable a => a -> (Symbol, Expr) -> a
F.subst1 SpecType
t ((Symbol, Expr) -> SpecType)
-> (Expr -> (Symbol, Expr)) -> Expr -> SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol
x,)) (CGEnv -> CoreExpr -> Maybe Expr
argExpr CGEnv
γ CoreExpr
a)
consE CGEnv
γ e' :: CoreExpr
e'@(App CoreExpr
e CoreExpr
a)
= do ([], [PVar (RType RTyCon RTyVar ())]
πs, SpecType
te) <- SpecType
-> ([(RTVar RTyVar (RType RTyCon RTyVar ()), RReft)],
[PVar (RType RTyCon RTyVar ())], SpecType)
forall tv c r.
RType tv c r
-> ([(RTVar c (RType tv c ()), r)], [PVar (RType tv c ())],
RType tv c r)
bkUniv (SpecType
-> ([(RTVar RTyVar (RType RTyCon RTyVar ()), RReft)],
[PVar (RType RTyCon RTyVar ())], SpecType))
-> CG SpecType
-> StateT
CGInfo
Identity
([(RTVar RTyVar (RType RTyCon RTyVar ()), RReft)],
[PVar (RType RTyCon RTyVar ())], SpecType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CGEnv -> CoreExpr -> CG SpecType
consE CGEnv
γ CoreExpr
e
SpecType
te1 <- CGEnv -> CoreExpr -> SpecType -> CG SpecType
instantiatePreds CGEnv
γ CoreExpr
e' (SpecType -> CG SpecType) -> SpecType -> CG SpecType
forall a b. (a -> b) -> a -> b
$ (PVar (RType RTyCon RTyVar ()) -> SpecType -> SpecType)
-> SpecType -> [PVar (RType RTyCon RTyVar ())] -> SpecType
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr PVar (RType RTyCon RTyVar ()) -> SpecType -> SpecType
forall c tv r. PVU c tv -> RType c tv r -> RType c tv r
RAllP SpecType
te [PVar (RType RTyCon RTyVar ())]
πs
(CGEnv
γ', SpecType
te2) <- CGEnv -> SpecType -> CG (CGEnv, SpecType)
dropExists CGEnv
γ SpecType
te1
SpecType
te3 <- CGEnv -> SpecType -> CG SpecType
dropConstraints CGEnv
γ SpecType
te2
Maybe SrcSpan -> SpecType -> State CGInfo ()
updateLocA (CoreExpr -> Maybe SrcSpan
exprLoc CoreExpr
e) SpecType
te3
let RFun Symbol
x RFInfo
_ SpecType
tx SpecType
t RReft
_ = ([Char], CoreExpr) -> CGEnv -> SpecType -> SpecType
forall a.
Outputable a =>
([Char], a) -> CGEnv -> SpecType -> SpecType
checkFun ([Char]
"Non-fun App with caller ", CoreExpr
e') CGEnv
γ SpecType
te3
CGEnv -> CoreExpr -> SpecType -> State CGInfo ()
cconsE CGEnv
γ' CoreExpr
a SpecType
tx
CGEnv -> CoreExpr -> SpecType -> SpecType
makeSingleton CGEnv
γ' (CoreExpr -> CoreExpr
simplify CoreExpr
e') (SpecType -> SpecType) -> CG SpecType -> CG SpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CGEnv -> SpecType -> CG SpecType
addPost CGEnv
γ' (SpecType -> (Expr -> SpecType) -> Maybe Expr -> 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
t CoreExpr
a) (SpecType -> (Symbol, Expr) -> SpecType
forall a. Subable a => a -> (Symbol, Expr) -> a
F.subst1 SpecType
t ((Symbol, Expr) -> SpecType)
-> (Expr -> (Symbol, Expr)) -> Expr -> SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol
x,)) (CGEnv -> CoreExpr -> Maybe Expr
argExpr CGEnv
γ (CoreExpr -> Maybe Expr) -> CoreExpr -> Maybe Expr
forall a b. (a -> b) -> a -> b
$ CoreExpr -> CoreExpr
simplify CoreExpr
a))
consE CGEnv
γ (Lam Id
α CoreExpr
e) | Id -> Bool
isTyVar Id
α
= do CGEnv
γ' <- CGEnv -> Id -> CG CGEnv
updateEnvironment CGEnv
γ Id
α
SpecType
t' <- CGEnv -> CoreExpr -> CG SpecType
consE CGEnv
γ' CoreExpr
e
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
$ RTVar RTyVar (RType RTyCon RTyVar ())
-> SpecType -> RReft -> SpecType
forall c tv r. RTVU c tv -> RType c tv r -> r -> RType c tv r
RAllT (RTyVar -> RTVar RTyVar (RType RTyCon RTyVar ())
forall tv s. tv -> RTVar tv s
makeRTVar (RTyVar -> RTVar RTyVar (RType RTyCon RTyVar ()))
-> RTyVar -> RTVar RTyVar (RType RTyCon RTyVar ())
forall a b. (a -> b) -> a -> b
$ Id -> RTyVar
rTyVar Id
α) SpecType
t' RReft
forall a. Monoid a => a
mempty
consE CGEnv
γ e :: CoreExpr
e@(Lam Id
x CoreExpr
e1)
= do SpecType
tx <- Bool -> KVKind -> CoreExpr -> Type -> CG SpecType
freshTyType (Config -> Bool
typeclass (CGEnv -> Config
forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)) KVKind
LamE (Id -> CoreExpr
forall b. Id -> Expr b
Var Id
x) Type
τx
CGEnv
γ' <- CGEnv
γ CGEnv -> ([Char], Symbol, SpecType) -> CG CGEnv
+= ([Char]
"consE", Id -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Id
x, SpecType
tx)
SpecType
t1 <- CGEnv -> CoreExpr -> CG SpecType
consE CGEnv
γ' CoreExpr
e1
Id -> Annot SpecType -> State CGInfo ()
addIdA Id
x (Annot SpecType -> State CGInfo ())
-> Annot SpecType -> State CGInfo ()
forall a b. (a -> b) -> a -> b
$ SpecType -> Annot SpecType
forall t. t -> Annot t
AnnDef SpecType
tx
WfC -> State CGInfo ()
addW (WfC -> State CGInfo ()) -> WfC -> State CGInfo ()
forall a b. (a -> b) -> a -> b
$ CGEnv -> SpecType -> WfC
WfC CGEnv
γ SpecType
tx
TCEmb TyCon
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
RReft
lamSing <- CGEnv -> TCEmb TyCon -> Id -> CoreExpr -> CG RReft
lambdaSingleton CGEnv
γ TCEmb TyCon
tce Id
x CoreExpr
e1
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
$ Symbol -> RFInfo -> SpecType -> SpecType -> RReft -> SpecType
forall c tv r.
Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun (Id -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Id
x) (Config -> RFInfo
mkRFInfo (Config -> RFInfo) -> Config -> RFInfo
forall a b. (a -> b) -> a -> b
$ CGEnv -> Config
forall t. HasConfig t => t -> Config
getConfig CGEnv
γ) SpecType
tx SpecType
t1 RReft
lamSing
where
FunTy { ft_arg :: Type -> Type
ft_arg = Type
τx } = (() :: Constraint) => 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 ((() :: Constraint) => 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 SpecType
t <- CGEnv -> CoreExpr -> CG SpecType
consE (CGEnv -> Span -> CGEnv
setLocation CGEnv
γ (CoreTickish -> Span
Sp.Tick CoreTickish
tt)) CoreExpr
e
Maybe Id -> SrcSpan -> Annot SpecType -> State CGInfo ()
addLocA Maybe Id
forall a. Maybe a
Nothing (CoreTickish -> SrcSpan
GM.tickSrcSpan CoreTickish
tt) (SpecType -> Annot SpecType
forall t. t -> Annot t
AnnUse SpecType
t)
SpecType -> CG SpecType
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return SpecType
t
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
γ ((() :: Constraint) => 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
$ (() :: Constraint) => CoreExpr -> Type
CoreExpr -> Type
exprType CoreExpr
e
consE CGEnv
_ e :: CoreExpr
e@(Type Type
t)
= Maybe SrcSpan -> [Char] -> CG SpecType
forall a. 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. 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
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
subsTyReft :: CGEnv -> RTyVar -> Type -> SpecType -> SpecType
subsTyReft :: CGEnv -> RTyVar -> Type -> SpecType -> SpecType
subsTyReft CGEnv
γ RTyVar
a Type
t = (Symbol -> Expr -> Expr) -> SpecType -> SpecType
forall c tv.
(Symbol -> Expr -> Expr) -> RType c tv RReft -> RType c tv RReft
mapExprReft (\Symbol
_ -> CoSub -> Expr -> Expr
F.applyCoSub CoSub
coSub)
where
coSub :: CoSub
coSub = [(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)]
consPattern :: CGEnv -> Rs.Pattern -> Type -> CG SpecType
consPattern :: CGEnv -> Pattern -> Type -> CG SpecType
consPattern CGEnv
γ (Rs.PatBind CoreExpr
e1 Id
x CoreExpr
e2 Type
_ CoreExpr
_ Type
_ Type
_ Id
_) Type
_ = do
SpecType
tx <- ([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
CGEnv
γ' <- CGEnv
γ CGEnv -> ([Char], Symbol, SpecType) -> CG CGEnv
+= ([Char]
"consPattern", Id -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Id
x, SpecType
tx)
Id -> Annot SpecType -> State CGInfo ()
addIdA Id
x (SpecType -> Annot SpecType
forall t. t -> Annot t
AnnDef SpecType
tx)
CGEnv -> CoreExpr -> CG SpecType
consE CGEnv
γ' CoreExpr
e2
where
msg :: a
msg = a
"This expression has a refined monadic type; run with --no-pattern-inline: "
consPattern CGEnv
γ (Rs.PatReturn CoreExpr
e Type
m CoreExpr
_ Type
_ Id
_) Type
t = do
SpecType
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
SpecType
mt <- Bool -> Type -> CG SpecType
trueTy (Config -> Bool
typeclass (CGEnv -> Config
forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)) Type
m
SpecType
tt <- Bool -> Type -> CG SpecType
trueTy (Config -> Bool
typeclass (CGEnv -> Config
forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)) Type
t
SpecType -> CG SpecType
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (SpecType -> SpecType -> SpecType -> SpecType
mkRAppTy SpecType
mt SpecType
et SpecType
tt)
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. (?callStack::CallStack) => [a] -> Int -> a
!! Int
i
SpecType
t <- (WfC -> State CGInfo ()
addW (WfC -> State CGInfo ())
-> (SpecType -> WfC) -> SpecType -> State CGInfo ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CGEnv -> SpecType -> WfC
WfC CGEnv
γ) (SpecType -> State CGInfo ()) -> CG SpecType -> CG SpecType
forall (m :: * -> *) b a. Monad m => (b -> m a) -> m b -> m b
<<= 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
τ
CGEnv
γ' <- CGEnv
-> Id -> [AltCon] -> AltCon -> [Id] -> Maybe [Int] -> CG CGEnv
caseEnv CGEnv
γ Id
xe [] (DataCon -> AltCon
DataAlt DataCon
c) [Id]
ys ([Int] -> Maybe [Int]
forall a. a -> Maybe a
Just [Int
i])
SpecType
ti <- (?callStack::CallStack) => CGEnv -> Id -> CG SpecType
CGEnv -> Id -> CG SpecType
varRefType CGEnv
γ' Id
yi
SubC -> [Char] -> State CGInfo ()
addC (CGEnv -> SpecType -> SpecType -> SubC
SubC CGEnv
γ' SpecType
ti SpecType
t) [Char]
"consPattern:project"
SpecType -> CG SpecType
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return SpecType
t
consPattern CGEnv
γ (Rs.PatSelfBind Id
_ CoreExpr
e) Type
_ =
CGEnv -> CoreExpr -> CG SpecType
consE CGEnv
γ CoreExpr
e
consPattern CGEnv
γ p :: Pattern
p@Rs.PatSelfRecBind{} Type
_ =
KVKind -> CGEnv -> CoreExpr -> CG SpecType
cconsFreshE KVKind
LetE CGEnv
γ (Pattern -> CoreExpr
Rs.lower Pattern
p)
mkRAppTy :: SpecType -> SpecType -> SpecType -> SpecType
mkRAppTy :: SpecType -> SpecType -> SpecType -> SpecType
mkRAppTy SpecType
mt SpecType
et RAppTy{} = SpecType -> SpecType -> RReft -> SpecType
forall c tv r. RType c tv r -> RType c tv r -> r -> RType 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 c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType 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. 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. (?callStack::CallStack) => [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 Maybe SpecType
mtc <- TyCon -> StateT CGInfo Identity (Maybe SpecType)
lookupNewType (CoAxiom Branched -> TyCon
forall (br :: BranchFlag). CoAxiom br -> TyCon
coAxiomTyCon CoAxiom Branched
ca)
Maybe SpecType -> (SpecType -> State CGInfo ()) -> State CGInfo ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
F.forM_ Maybe SpecType
mtc (CGEnv -> CoreExpr -> SpecType -> State CGInfo ()
cconsE CGEnv
γ CoreExpr
e)
CGEnv -> Type -> CoreExpr -> CG SpecType
castTy' CGEnv
γ Type
t CoreExpr
e
castTy CGEnv
γ Type
t CoreExpr
e CoercionR
_
= CGEnv -> Type -> CoreExpr -> CG SpecType
castTy' CGEnv
γ Type
t CoreExpr
e
castTy' :: CGEnv -> Type -> CoreExpr -> CG SpecType
castTy' CGEnv
γ Type
τ (Var Id
x)
= do SpecType
t0 <- Bool -> Type -> CG SpecType
trueTy (Config -> Bool
typeclass (CGEnv -> Config
forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)) Type
τ
SpecType
tx <- (?callStack::CallStack) => CGEnv -> Id -> CG SpecType
CGEnv -> Id -> CG SpecType
varRefType CGEnv
γ Id
x
let t :: SpecType
t = SpecType -> SpecType -> SpecType
mergeCastTys SpecType
t0 SpecType
tx
let ce :: Expr
ce = if Config -> Bool
typeclass (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 -> Expr
forall a. Expression a => a -> Expr
F.expr Id
x
else Sort -> Sort -> Expr -> Expr
eCoerc (TCEmb TyCon -> Type -> Sort
typeSort (CGEnv -> TCEmb TyCon
emb CGEnv
γ) (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
τ)
(Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Id -> Expr
forall a. Expression a => a -> Expr
F.expr Id
x
SpecType -> CG SpecType
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (SpecType
t SpecType -> RReft -> SpecType
forall r c tv. Reftable r => RType c tv r -> r -> RType c tv r
`strengthen` Reft -> RReft
forall r. r -> UReft r
uTop (Expr -> Reft
forall a. Expression a => a -> Reft
F.uexprReft Expr
ce) )
where eCoerc :: Sort -> Sort -> Expr -> Expr
eCoerc Sort
s Sort
t Expr
e
| Sort
s Sort -> Sort -> Bool
forall a. Eq a => a -> a -> Bool
== Sort
t = Expr
e
| Bool
otherwise = Sort -> Sort -> Expr -> Expr
F.ECoerc Sort
s Sort
t Expr
e
castTy' CGEnv
γ Type
t (Tick CoreTickish
_ CoreExpr
e)
= CGEnv -> Type -> CoreExpr -> CG SpecType
castTy' CGEnv
γ Type
t CoreExpr
e
castTy' CGEnv
_ Type
_ CoreExpr
e
= Maybe SrcSpan -> [Char] -> CG SpecType
forall a. 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 :: 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 c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType 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
isClassConCo :: Coercion -> Maybe (Expr Var -> Expr Var)
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)
, 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
cconsFreshE :: KVKind -> CGEnv -> CoreExpr -> CG SpecType
cconsFreshE :: KVKind -> CGEnv -> CoreExpr -> CG SpecType
cconsFreshE KVKind
kvkind CGEnv
γ CoreExpr
e = do
SpecType
t <- Bool -> KVKind -> CoreExpr -> Type -> CG SpecType
freshTyType (Config -> Bool
typeclass (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
$ (() :: Constraint) => CoreExpr -> Type
CoreExpr -> Type
exprType CoreExpr
e
WfC -> State CGInfo ()
addW (WfC -> State CGInfo ()) -> WfC -> State CGInfo ()
forall a b. (a -> b) -> a -> b
$ CGEnv -> SpecType -> WfC
WfC CGEnv
γ SpecType
t
CGEnv -> CoreExpr -> SpecType -> State CGInfo ()
cconsE CGEnv
γ CoreExpr
e SpecType
t
SpecType -> CG SpecType
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return SpecType
t
checkUnbound :: (Show a, Show a2, F.Subable a)
=> CGEnv -> CoreExpr -> F.Symbol -> a -> a2 -> a
checkUnbound :: forall a a2.
(Show a, Show a2, Subable a) =>
CGEnv -> CoreExpr -> Symbol -> a -> a2 -> a
checkUnbound CGEnv
γ CoreExpr
e Symbol
x a
t a2
a
| Symbol
x 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. 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 c tv r.
Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
x RFInfo
i SpecType
tx) RReft
r (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
γ' <- (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
SubC -> [Char] -> State CGInfo ()
addC (CGEnv -> SpecType -> SpecType -> SubC
SubC CGEnv
γ' SpecType
t1 SpecType
t2) [Char]
"dropConstraints"
CGEnv -> SpecType -> CG SpecType
dropConstraints CGEnv
cgenv SpecType
rt
where
([(Symbol, SpecType)]
xts, SpecType
t1, SpecType
t2) = [(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 CGEnv
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
CGEnv -> CoreExpr -> SpecType -> State CGInfo ()
cconsE CGEnv
cγ CoreExpr
ce SpecType
t
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)
SpecType
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
γ (?callStack::CallStack) => CGEnv -> Id -> CG SpecType
CGEnv -> Id -> CG SpecType
??= Id
x
let rt :: SpecType
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'
SpecType
tdc <- CGEnv
γ (?callStack::CallStack) => CGEnv -> Id -> CG SpecType
CGEnv -> Id -> CG SpecType
??= DataCon -> Id
dataConWorkId DataCon
c CG SpecType -> (SpecType -> CG SpecType) -> CG SpecType
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 -> CG SpecType
forall (m :: * -> *). FreshM m => SpecType -> m SpecType
refreshVV
let (SpecType
rtd,[SpecType]
yts',SpecType
_) = SpecType -> SpecType -> [Id] -> (SpecType, [SpecType], SpecType)
unfoldR SpecType
tdc SpecType
rt [Id]
ys
[SpecType]
yts <- Bool
-> Maybe [Int] -> [SpecType] -> StateT CGInfo Identity [SpecType]
projectTypes (Config -> Bool
typeclass (CGEnv -> Config
forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)) Maybe [Int]
pIs [SpecType]
yts'
let ys'' :: [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 -> 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 :: Reft
r1 = DataCon -> [Symbol] -> Reft
dataConReft DataCon
c [Symbol]
ys''
let r2 :: Reft
r2 = SpecType -> [Symbol] -> Reft
forall r c tv. Reftable r => RType c tv r -> [Symbol] -> Reft
dataConMsReft SpecType
rtd [Symbol]
ys''
let xt :: SpecType
xt = (SpecType
xt0 SpecType -> SpecType -> SpecType
forall r. Reftable r => r -> r -> r
`F.meet` SpecType
rtd) SpecType -> RReft -> SpecType
forall r c tv. Reftable r => RType c tv r -> r -> RType c tv r
`strengthen` Reft -> RReft
forall r. r -> UReft r
uTop (Reft
r1 Reft -> Reft -> Reft
forall r. Reftable r => r -> r -> r
`F.meet` Reft
r2)
let cbs :: [(Symbol, SpecType)]
cbs = [Char] -> [Symbol] -> [SpecType] -> [(Symbol, SpecType)]
forall a b.
(?callStack::CallStack) =>
[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, Expr) -> SpecType
forall a. Subable a => a -> (Symbol, Expr) -> a
`F.subst1` (Symbol
selfSymbol, Symbol -> Expr
F.EVar Symbol
x'))
(SpecType
xt0 SpecType -> [SpecType] -> [SpecType]
forall a. a -> [a] -> [a]
: [SpecType]
yts))
CGEnv
cγ' <- CGEnv -> Symbol -> [(Symbol, SpecType)] -> CG CGEnv
addBinders CGEnv
γ Symbol
x' [(Symbol, SpecType)]
cbs
CGEnv -> Symbol -> [(Symbol, SpecType)] -> CG CGEnv
addBinders CGEnv
cγ' Symbol
x' [(Symbol
x', RReft -> RReft
substSelf (RReft -> RReft) -> SpecType -> SpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SpecType
xt)]
where allowTC :: Bool
allowTC = Config -> Bool
typeclass (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
SpecType
xt' <- (SpecType -> RReft -> SpecType
forall r c tv. Reftable r => RType c tv r -> r -> RType c tv r
`strengthen` Reft -> RReft
forall r. r -> UReft 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
γ (?callStack::CallStack) => CGEnv -> Id -> CG SpecType
CGEnv -> Id -> CG SpecType
??= Id
x)
CGEnv -> Symbol -> [(Symbol, SpecType)] -> CG CGEnv
addBinders CGEnv
γ Symbol
x' [(Symbol
x', SpecType
xt')]
substSelf :: UReft F.Reft -> UReft F.Reft
substSelf :: RReft -> RReft
substSelf (MkUReft Reft
r Predicate
p) = Reft -> Predicate -> RReft
forall r. r -> Predicate -> UReft r
MkUReft (Reft -> Reft
substSelfReft Reft
r) Predicate
p
substSelfReft :: F.Reft -> F.Reft
substSelfReft :: Reft -> Reft
substSelfReft (F.Reft (Symbol
v, Expr
e)) = (Symbol, Expr) -> Reft
F.Reft (Symbol
v, Expr -> (Symbol, Expr) -> Expr
forall a. Subable a => a -> (Symbol, Expr) -> a
F.subst1 Expr
e (Symbol
selfSymbol, Symbol -> Expr
F.EVar Symbol
v))
ignoreSelf :: F.Reft -> F.Reft
ignoreSelf :: Reft -> Reft
ignoreSelf = (Expr -> Expr) -> Reft -> Reft
forall t. Visitable t => (Expr -> Expr) -> t -> t
F.mapExpr (\Expr
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` Expr -> [Symbol]
forall a. Subable a => a -> [Symbol]
F.syms Expr
r then Expr
F.PTrue else Expr
r)
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 -> (Expr -> Reft) -> Maybe Expr -> Reft
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Reft
forall a. Monoid a => a
mempty Expr -> Reft
forall a. Expression a => a -> Reft
F.notExprReft (Maybe Expr -> Reft) -> (Literal -> Maybe Expr) -> Literal -> Reft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Sort, Maybe Expr) -> Maybe Expr
forall a b. (a, b) -> b
snd ((Sort, Maybe Expr) -> Maybe Expr)
-> (Literal -> (Sort, Maybe Expr)) -> Literal -> Maybe Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCEmb TyCon -> Literal -> (Sort, Maybe Expr)
literalConst (CGEnv -> TCEmb TyCon
emb CGEnv
γ)
notDataConReft :: DataCon -> Reft
notDataConReft DataCon
d | Config -> Bool
exactDC (CGEnv -> Config
forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)
= (Symbol, Expr) -> Reft
F.Reft (Symbol
F.vv_, Expr -> Expr
F.PNot (Expr -> Expr -> Expr
F.EApp (Symbol -> Expr
F.EVar (Symbol -> Expr) -> Symbol -> Expr
forall a b. (a -> b) -> a -> b
$ DataCon -> Symbol
makeDataConChecker DataCon
d) (Symbol -> Expr
F.EVar Symbol
F.vv_)))
| Bool
otherwise = Reft
forall a. Monoid a => a
mempty
altReft CGEnv
_ [AltCon]
_ AltCon
_ = Maybe SrcSpan -> [Char] -> Reft
forall a. 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 {c} {tv} {r}. RType c tv r -> RType c tv r
ignoreOblig SpecType
rt)
where
tbody :: SpecType
tbody = SpecType -> [RTProp RTyCon RTyVar RReft] -> SpecType
instantiatePvs (SpecType -> [SpecType] -> SpecType
instantiateTys SpecType
td [SpecType]
ts) ([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'' = (Subst -> SpecType -> SpecType)
-> [Subst] -> [SpecType] -> [SpecType]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Subst -> SpecType -> SpecType
forall a. Subable a => Subst -> a -> a
F.subst [Subst]
sus ([SpecType]
yts'[SpecType] -> [SpecType] -> [SpecType]
forall a. [a] -> [a] -> [a]
++[SpecType
rt])
(SpecType
t3,[SpecType]
yts) = ([SpecType] -> SpecType
forall a. (?callStack::CallStack) => [a] -> a
last [SpecType]
yts'', [SpecType] -> [SpecType]
forall a. (?callStack::CallStack) => [a] -> [a]
init [SpecType]
yts'')
sus :: [Subst]
sus = [(Symbol, Expr)] -> Subst
F.mkSubst ([(Symbol, Expr)] -> Subst) -> [[(Symbol, Expr)]] -> [Subst]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, Expr)] -> [[(Symbol, Expr)]]
forall a. [a] -> [[a]]
L.inits [(Symbol
x, Symbol -> Expr
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], [Id]) -> ([Id], [Symbol])
forall b c a. (b -> c) -> (a, b) -> (a, c)
mapSnd (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], [Id]) -> ([Id], [Symbol]))
-> ([Id], [Id]) -> ([Id], [Symbol])
forall a b. (a -> b) -> a -> 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. 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 ()))) =>
RType c tv r -> RType c tv r -> RType c tv r
go
where
go :: RType c tv r -> RType c tv r -> RType c tv r
go (RAllT RTVar tv (RType c tv ())
α RType c tv r
tbody r
_) RType c tv r
t = (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
tbody
go RType c tv r
_ RType c tv r
_ = Maybe SrcSpan -> [Char] -> RType c tv r
forall a. 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 PVar (RType RTyCon RTyVar ())
p SpecType
tbody) RTProp RTyCon RTyVar RReft
r = [Char]
-> SpecType
-> [(PVar (RType RTyCon RTyVar ()), RTProp RTyCon RTyVar RReft)]
-> SpecType
replacePreds [Char]
"instantiatePv" SpecType
tbody [(PVar (RType RTyCon RTyVar ())
p, RTProp RTyCon RTyVar RReft
r)]
go SpecType
t RTProp RTyCon RTyVar RReft
_ = [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. 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
freshPredRef :: CGEnv -> CoreExpr -> PVar RSort -> CG SpecProp
freshPredRef :: CGEnv
-> CoreExpr
-> PVar (RType RTyCon RTyVar ())
-> CG (RTProp RTyCon RTyVar RReft)
freshPredRef CGEnv
γ CoreExpr
e (PV Symbol
_ (PVProp RType RTyCon RTyVar ()
rsort) Symbol
_ [(RType RTyCon RTyVar (), Symbol, Expr)]
as)
= do SpecType
t <- Bool -> KVKind -> CoreExpr -> Type -> CG SpecType
freshTyType (Config -> Bool
typeclass (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)
[Symbol]
args <- ((RType RTyCon RTyVar (), Symbol, Expr)
-> StateT CGInfo Identity Symbol)
-> [(RType RTyCon RTyVar (), Symbol, Expr)]
-> StateT CGInfo Identity [Symbol]
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 (StateT CGInfo Identity Symbol
-> (RType RTyCon RTyVar (), Symbol, Expr)
-> StateT CGInfo Identity Symbol
forall a b. a -> b -> a
const StateT CGInfo Identity Symbol
forall (m :: * -> *) a. Freshable m a => m a
fresh) [(RType RTyCon RTyVar (), Symbol, Expr)]
as
let targs :: [(Symbol, RType RTyCon RTyVar ())]
targs = [(Symbol
x, RType RTyCon RTyVar ()
s) | (Symbol
x, (RType RTyCon RTyVar ()
s, Symbol
y, Expr
z)) <- [Symbol]
-> [(RType RTyCon RTyVar (), Symbol, Expr)]
-> [(Symbol, (RType RTyCon RTyVar (), Symbol, Expr))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
args [(RType RTyCon RTyVar (), Symbol, Expr)]
as, Symbol -> Expr
F.EVar Symbol
y Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
z ]
CGEnv
γ' <- (CGEnv -> ([Char], Symbol, SpecType) -> CG CGEnv)
-> CGEnv -> [([Char], Symbol, SpecType)] -> CG CGEnv
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM CGEnv -> ([Char], Symbol, SpecType) -> CG CGEnv
(+=) CGEnv
γ [([Char]
"freshPredRef", Symbol
x, RType RTyCon RTyVar () -> SpecType
forall r c tv. Reftable r => RType c tv () -> RType c tv r
ofRSort RType RTyCon RTyVar ()
τ) | (Symbol
x, RType RTyCon RTyVar ()
τ) <- [(Symbol, RType RTyCon RTyVar ())]
targs]
WfC -> State CGInfo ()
addW (WfC -> State CGInfo ()) -> WfC -> State CGInfo ()
forall a b. (a -> b) -> a -> b
$ CGEnv -> SpecType -> WfC
WfC CGEnv
γ' SpecType
t
RTProp RTyCon RTyVar RReft -> CG (RTProp RTyCon RTyVar RReft)
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (RTProp RTyCon RTyVar RReft -> CG (RTProp RTyCon RTyVar RReft))
-> RTProp RTyCon RTyVar RReft -> CG (RTProp RTyCon RTyVar RReft)
forall a b. (a -> b) -> a -> b
$ [(Symbol, RType RTyCon RTyVar ())]
-> SpecType -> RTProp RTyCon RTyVar RReft
forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp [(Symbol, RType RTyCon RTyVar ())]
targs SpecType
t
freshPredRef CGEnv
_ CoreExpr
_ (PV Symbol
_ PVKind (RType RTyCon RTyVar ())
PVHProp Symbol
_ [(RType RTyCon RTyVar (), Symbol, Expr)]
_)
= Maybe SrcSpan -> [Char] -> CG (RTProp RTyCon RTyVar RReft)
forall a. Maybe SrcSpan -> [Char] -> a
todo Maybe SrcSpan
forall a. Maybe a
Nothing [Char]
"EFFECTS:freshPredRef"
argType :: Type -> Maybe F.Expr
argType :: Type -> Maybe Expr
argType (LitTy (NumTyLit Integer
i)) = Integer -> Maybe Expr
mkI Integer
i
argType (LitTy (StrTyLit FastString
s)) = ByteString -> Maybe Expr
mkS (ByteString -> Maybe Expr) -> ByteString -> Maybe Expr
forall a b. (a -> b) -> a -> b
$ FastString -> ByteString
bytesFS FastString
s
argType (TyVarTy Id
x) = Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> Maybe Expr) -> Expr -> Maybe Expr
forall a b. (a -> b) -> a -> b
$ Symbol -> Expr
F.EVar (Symbol -> Expr) -> Symbol -> Expr
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
= Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> Maybe Expr) -> Expr -> Maybe Expr
forall a b. (a -> b) -> a -> b
$ Symbol -> Expr
F.EVar Symbol
anyTypeSymbol
argType Type
_ = Maybe Expr
forall a. Maybe a
Nothing
argExpr :: CGEnv -> CoreExpr -> Maybe F.Expr
argExpr :: CGEnv -> CoreExpr -> Maybe Expr
argExpr CGEnv
_ (Var Id
v) = Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> Maybe Expr) -> Expr -> Maybe Expr
forall a b. (a -> b) -> a -> b
$ Id -> Expr
forall a. Symbolic a => a -> Expr
F.eVar Id
v
argExpr CGEnv
γ (Lit Literal
c) = (Sort, Maybe Expr) -> Maybe Expr
forall a b. (a, b) -> b
snd ((Sort, Maybe Expr) -> Maybe Expr)
-> (Sort, Maybe Expr) -> Maybe Expr
forall a b. (a -> b) -> a -> b
$ TCEmb TyCon -> Literal -> (Sort, Maybe Expr)
literalConst (CGEnv -> TCEmb TyCon
emb CGEnv
γ) Literal
c
argExpr CGEnv
γ (Tick CoreTickish
_ CoreExpr
e) = CGEnv -> CoreExpr -> Maybe Expr
argExpr CGEnv
γ CoreExpr
e
argExpr CGEnv
γ (App CoreExpr
e (Type Type
_)) = CGEnv -> CoreExpr -> Maybe Expr
argExpr CGEnv
γ CoreExpr
e
argExpr CGEnv
_ CoreExpr
_ = Maybe Expr
forall a. Maybe a
Nothing
lamExpr :: CGEnv -> CoreExpr -> CG (Maybe F.Expr)
lamExpr :: CGEnv -> CoreExpr -> CG (Maybe Expr)
lamExpr CGEnv
g CoreExpr
e = do
[DataDecl]
adts <- (CGInfo -> [DataDecl]) -> StateT CGInfo Identity [DataDecl]
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CGInfo -> [DataDecl]
cgADTs
Bool
allowTC <- (CGInfo -> Bool) -> StateT CGInfo Identity Bool
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CGInfo -> Bool
cgiTypeclass
let dm :: DataConMap
dm = [DataDecl] -> DataConMap
dataConMap [DataDecl]
adts
Maybe Expr -> CG (Maybe Expr)
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Expr -> CG (Maybe Expr)) -> Maybe Expr -> CG (Maybe Expr)
forall a b. (a -> b) -> a -> b
$ Either (TError SpecType) Expr -> Maybe Expr
forall a b. Either a b -> Maybe b
eitherToMaybe (Either (TError SpecType) Expr -> Maybe Expr)
-> Either (TError SpecType) Expr -> Maybe Expr
forall a b. (a -> b) -> a -> b
$ TCEmb TyCon
-> LogicMap
-> DataConMap
-> ([Char] -> TError SpecType)
-> LogicM Expr
-> Either (TError SpecType) Expr
forall t.
TCEmb TyCon
-> LogicMap
-> DataConMap
-> ([Char] -> TError SpecType)
-> LogicM t
-> Either (TError SpecType) t
runToLogic (CGEnv -> TCEmb TyCon
emb CGEnv
g) LogicMap
forall a. Monoid a => a
mempty DataConMap
dm
(\[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))
(Bool -> CoreExpr -> LogicM Expr
coreToLogic Bool
allowTC CoreExpr
e)
(??=) :: (?callStack :: CallStack) => CGEnv -> Var -> CG SpecType
CGEnv
γ ??= :: (?callStack::CallStack) => CGEnv -> Id -> CG SpecType
??= Id
x = case 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
γ (?callStack::CallStack) => 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 :: (?callStack::CallStack) => 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
γ (?callStack::CallStack) => CGEnv -> Id -> CG SpecType
CGEnv -> Id -> CG SpecType
??= Id
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
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 Expr
funExpr CGEnv
γ CoreExpr
f, CoreExpr -> Maybe Expr
argForAllExpr CoreExpr
x) of
(Just Expr
f', Just Expr
x')
| Bool -> Bool
not (if Config -> Bool
typeclass (CGEnv -> Config
forall t. HasConfig t => t -> Config
getConfig CGEnv
γ) then CoreExpr -> Bool
GM.isEmbeddedDictExpr CoreExpr
x else CoreExpr -> Bool
GM.isPredExpr CoreExpr
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. r -> UReft r
uTop (Reft -> RReft) -> Reft -> RReft
forall a b. (a -> b) -> a -> b
$ Expr -> Reft
forall a. Expression a => a -> Reft
F.exprReft (Expr -> Expr -> Expr
F.EApp Expr
f' Expr
x'))
(Just Expr
f', Just Expr
_)
-> 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. r -> UReft r
uTop (Reft -> RReft) -> Reft -> RReft
forall a b. (a -> b) -> a -> b
$ Expr -> Reft
forall a. Expression a => a -> Reft
F.exprReft Expr
f')
(Maybe Expr, Maybe Expr)
_ -> SpecType
t
| Config -> Bool
rankNTypes (CGEnv -> Config
forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)
= case CGEnv -> CoreExpr -> Maybe Expr
argExpr CGEnv
γ (CoreExpr -> CoreExpr
simplify CoreExpr
cexpr) of
Just Expr
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. r -> UReft r
uTop (Expr -> Reft
forall a. Expression a => a -> Reft
F.exprReft Expr
e')
Maybe Expr
_ -> SpecType
t
| Bool
otherwise
= SpecType
t
where
argForAllExpr :: CoreExpr -> Maybe Expr
argForAllExpr (Var Id
x)
| Config -> Bool
rankNTypes (CGEnv -> Config
forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)
, Just Expr
e <- Id -> HashMap Id Expr -> Maybe Expr
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup Id
x (CGEnv -> HashMap Id Expr
forallcb CGEnv
γ)
= Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
e
argForAllExpr CoreExpr
e
= CGEnv -> CoreExpr -> Maybe Expr
argExpr CGEnv
γ CoreExpr
e
funExpr :: CGEnv -> CoreExpr -> Maybe F.Expr
funExpr :: CGEnv -> CoreExpr -> Maybe Expr
funExpr CGEnv
_ (Var Id
v)
= Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> Maybe Expr) -> Expr -> Maybe Expr
forall a b. (a -> b) -> a -> b
$ Symbol -> Expr
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 Expr
funExpr CGEnv
γ CoreExpr
e1, CGEnv -> CoreExpr -> Maybe Expr
argExpr CGEnv
γ CoreExpr
e2) of
(Just Expr
e1', Just Expr
e2') | Bool -> Bool
not (if Config -> Bool
typeclass (CGEnv -> Config
forall t. HasConfig t => t -> Config
getConfig CGEnv
γ) then CoreExpr -> Bool
GM.isEmbeddedDictExpr CoreExpr
e2
else CoreExpr -> Bool
GM.isPredExpr CoreExpr
e2)
-> Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> Expr -> Expr
F.EApp Expr
e1' Expr
e2')
(Just Expr
e1', Just Expr
_) -> Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
e1'
(Maybe Expr, Maybe Expr)
_ -> Maybe Expr
forall a. Maybe a
Nothing
funExpr CGEnv
_ CoreExpr
_
= Maybe Expr
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. r -> UReft 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
strengthenTop :: (PPrint r, F.Reftable r) => RType c tv r -> r -> RType c tv r
strengthenTop :: forall {r} {c} {tv}.
(PPrint r, Reftable r) =>
RType c tv r -> r -> RType c tv r
strengthenTop (RApp c
c [RType c tv r]
ts [RTProp c tv r]
rs r
r) r
r' = c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp c
c [RType c tv r]
ts [RTProp c tv r]
rs (r -> RType c tv r) -> r -> RType c tv r
forall a b. (a -> b) -> a -> b
$ r -> r -> r
forall r. Reftable r => r -> r -> r
F.meet r
r r
r'
strengthenTop (RVar tv
a r
r) r
r' = tv -> r -> RType c tv r
forall c tv r. tv -> r -> RType c tv r
RVar tv
a (r -> RType c tv r) -> r -> RType c tv r
forall a b. (a -> b) -> a -> b
$ r -> r -> r
forall r. Reftable r => r -> r -> r
F.meet r
r r
r'
strengthenTop (RFun Symbol
b RFInfo
i RType c tv r
t1 RType c tv r
t2 r
r) r
r' = Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
forall c tv r.
Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
b RFInfo
i RType c tv r
t1 RType c tv r
t2 (r -> RType c tv r) -> r -> RType c tv r
forall a b. (a -> b) -> a -> b
$ r -> r -> r
forall r. Reftable r => r -> r -> r
F.meet r
r r
r'
strengthenTop (RAppTy RType c tv r
t1 RType c tv r
t2 r
r) r
r' = RType c tv r -> RType c tv r -> r -> RType c tv r
forall c tv r. RType c tv r -> RType c tv r -> r -> RType c tv r
RAppTy RType c tv r
t1 RType c tv r
t2 (r -> RType c tv r) -> r -> RType c tv r
forall a b. (a -> b) -> a -> b
$ r -> r -> r
forall r. Reftable r => r -> r -> r
F.meet r
r r
r'
strengthenTop (RAllT RTVU c tv
a RType c tv r
t r
r) r
r' = RTVU c tv -> RType c tv r -> r -> RType c tv r
forall c tv r. RTVU c tv -> RType c tv r -> r -> RType c tv r
RAllT RTVU c tv
a RType c tv r
t (r -> RType c tv r) -> r -> RType c tv r
forall a b. (a -> b) -> a -> b
$ r -> r -> r
forall r. Reftable r => r -> r -> r
F.meet r
r r
r'
strengthenTop RType c tv r
t r
_ = RType c tv r
t
strengthenMeet :: (PPrint r, F.Reftable r) => RType c tv r -> r -> RType c tv r
strengthenMeet :: forall {r} {c} {tv}.
(PPrint r, Reftable r) =>
RType c tv r -> r -> RType c tv r
strengthenMeet (RApp c
c [RType c tv r]
ts [RTProp c tv r]
rs r
r) r
r' = c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp c
c [RType c tv r]
ts [RTProp c tv r]
rs (r
r r -> r -> r
forall r. Reftable r => r -> r -> r
`F.meet` r
r')
strengthenMeet (RVar tv
a r
r) r
r' = tv -> r -> RType c tv r
forall c tv r. tv -> r -> RType c tv r
RVar tv
a (r
r r -> r -> r
forall r. Reftable r => r -> r -> r
`F.meet` r
r')
strengthenMeet (RFun Symbol
b RFInfo
i RType c tv r
t1 RType c tv r
t2 r
r) r
r'= Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
forall c tv r.
Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
b RFInfo
i RType c tv r
t1 RType c tv r
t2 (r
r r -> r -> r
forall r. Reftable r => r -> r -> r
`F.meet` r
r')
strengthenMeet (RAppTy RType c tv r
t1 RType c tv r
t2 r
r) r
r' = RType c tv r -> RType c tv r -> r -> RType c tv r
forall c tv r. RType c tv r -> RType c tv r -> r -> RType c tv r
RAppTy RType c tv r
t1 RType c tv r
t2 (r
r r -> r -> r
forall r. Reftable r => r -> r -> r
`F.meet` r
r')
strengthenMeet (RAllT RTVU c tv
a RType c tv r
t r
r) r
r' = RTVU c tv -> RType c tv r -> r -> RType c tv r
forall c tv r. RTVU c tv -> RType c tv r -> r -> RType c tv r
RAllT RTVU c tv
a (RType c tv r -> r -> RType c tv r
forall {r} {c} {tv}.
(PPrint r, Reftable r) =>
RType c tv r -> r -> RType c tv r
strengthenMeet RType c tv r
t r
r') (r
r r -> r -> r
forall r. Reftable r => r -> r -> r
`F.meet` r
r')
strengthenMeet RType c tv r
t r
_ = RType c tv r
t
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 ((() :: Constraint) => CoreExpr -> Type
CoreExpr -> Type
exprType CoreExpr
a) Type
predType
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 c r. Eq tv => RType c tv r -> [RTVar tv (RType c tv ())]
freeTyVars RType RTyCon b r
t']
isGenericClass :: Class -> Bool
isGenericClass Class
c = Class -> Name
className Class
c 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]
instance MonadFail Data.Functor.Identity.Identity where
fail :: forall a. [Char] -> Identity a
fail [Char]
msg = Maybe SrcSpan -> [Char] -> Identity a
forall a. Maybe SrcSpan -> [Char] -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing [Char]
msg