{-# LANGUAGE CPP                       #-}
{-# LANGUAGE DeriveFoldable            #-}
{-# LANGUAGE DeriveTraversable         #-}
{-# LANGUAGE StandaloneDeriving        #-}
{-# LANGUAGE ScopedTypeVariables       #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE TypeSynonymInstances      #-}
{-# LANGUAGE FlexibleContexts          #-}
{-# LANGUAGE FlexibleInstances         #-}
{-# LANGUAGE TupleSections             #-}
{-# LANGUAGE BangPatterns              #-}
{-# LANGUAGE PatternGuards             #-}
{-# LANGUAGE DeriveFunctor             #-}
{-# LANGUAGE MultiParamTypeClasses     #-}
{-# LANGUAGE OverloadedStrings         #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE ImplicitParams            #-}

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

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

#if !MIN_VERSION_base(4,14,0)
import Control.Monad.Fail
#endif

import           Outputable                                    (Outputable)
import           Prelude                                       hiding (error)
import           GHC.Stack
import           CoreUtils                                     (exprType)
import           MkCore
import           Coercion
import           DataCon
import           Pair
import           CoreSyn
import           SrcLoc                                 hiding (Located)
import           Type
import           VarEnv (mkRnEnv2, emptyInScopeSet)
import           TyCon
import           CoAxiom
import           PrelNames
import           Language.Haskell.Liquid.GHC.API               as Ghc hiding (exprType)
import           Language.Haskell.Liquid.GHC.TypeRep           ()
import           IdInfo
import           Unify
import           UniqSet (mkUniqSet)
import           Text.PrettyPrint.HughesPJ hiding ((<>)) 
import           Control.Monad.State
import           Data.Maybe                                    (fromMaybe, catMaybes, isJust)
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.Traversable                              as T
import qualified Data.Functor.Identity
import           Language.Fixpoint.Misc
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
import           Language.Haskell.Liquid.Constraint.Init
import           Language.Haskell.Liquid.Constraint.Env
import           Language.Haskell.Liquid.Constraint.Monad
import           Language.Haskell.Liquid.Constraint.Split
import           Language.Haskell.Liquid.Types.Dictionaries
import           Language.Haskell.Liquid.GHC.Play          (isHoleVar) 
import qualified Language.Haskell.Liquid.GHC.Resugar           as Rs
import qualified Language.Haskell.Liquid.GHC.SpanStack         as Sp
import qualified Language.Haskell.Liquid.GHC.Misc         as GM -- ( isInternal, collectArguments, tickSrcSpan, showPpr )
import           Language.Haskell.Liquid.Misc
import           Language.Haskell.Liquid.Constraint.Types
import           Language.Haskell.Liquid.Constraint.Constraint
import           Language.Haskell.Liquid.Transforms.Rec
import           Language.Haskell.Liquid.Transforms.CoreToLogic (weakenResult)
import           Language.Haskell.Liquid.Bare.DataType (makeDataConChecker)

import           Language.Haskell.Liquid.Types hiding (binds, Loc, loc, Def)

--------------------------------------------------------------------------------
-- | Constraint Generation: Toplevel -------------------------------------------
--------------------------------------------------------------------------------
generateConstraints      :: TargetInfo -> CGInfo
--------------------------------------------------------------------------------
generateConstraints :: TargetInfo -> CGInfo
generateConstraints TargetInfo
info = {-# SCC "ConsGen" #-} State CGInfo () -> CGInfo -> CGInfo
forall s a. State s a -> s -> s
execState State CGInfo ()
act (CGInfo -> CGInfo) -> CGInfo -> CGInfo
forall a b. (a -> b) -> a -> b
$ Config -> TargetInfo -> CGInfo
initCGI Config
cfg TargetInfo
info
  where
    act :: State CGInfo ()
act                  = do { 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

generateConstraintsWithEnv :: TargetInfo -> CGInfo -> CGEnv -> CGInfo
--------------------------------------------------------------------------------
generateConstraintsWithEnv :: TargetInfo -> CGInfo -> CGEnv -> CGInfo
generateConstraintsWithEnv TargetInfo
info CGInfo
cgi CGEnv
γ = {-# SCC "ConsGenEnv" #-} State CGInfo () -> CGInfo -> CGInfo
forall s a. State s a -> s -> s
execState State CGInfo ()
act CGInfo
cgi
  where
    act :: State CGInfo ()
act                  = 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) (((Var, Located SpecType) -> State CGInfo ())
-> [(Var, 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 ())
-> ((Var, Located SpecType) -> WfC)
-> (Var, Located SpecType)
-> State CGInfo ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CGEnv -> SpecType -> WfC
WfC CGEnv
γ (SpecType -> WfC)
-> ((Var, Located SpecType) -> SpecType)
-> (Var, 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)
-> ((Var, Located SpecType) -> Located SpecType)
-> (Var, Located SpecType)
-> SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Var, Located SpecType) -> Located SpecType
forall a b. (a, b) -> b
snd) (GhcSpecSig -> [(Var, Located SpecType)]
gsTySigs GhcSpecSig
sSpc [(Var, Located SpecType)]
-> [(Var, Located SpecType)] -> [(Var, Located SpecType)]
forall a. [a] -> [a] -> [a]
++ GhcSpecSig -> [(Var, Located SpecType)]
gsAsmSigs GhcSpecSig
sSpc))
  (CGEnv -> CoreBind -> CG CGEnv)
-> CGEnv -> [CoreBind] -> State CGInfo ()
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m ()
foldM_ (Config -> TargetInfo -> CGEnv -> CoreBind -> CG CGEnv
consCBTop Config
cfg TargetInfo
info) CGEnv
γ (TargetSrc -> [CoreBind]
giCbs TargetSrc
gSrc)
  ((Var, MethodType (Located SpecType)) -> State CGInfo ())
-> [(Var, MethodType (Located SpecType))]
-> StateT CGInfo Identity [()]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (CGEnv -> (Var, MethodType (Located SpecType)) -> State CGInfo ()
consClass CGEnv
γ) (GhcSpecSig -> [(Var, MethodType (Located SpecType))]
gsMethods (GhcSpecSig -> [(Var, MethodType (Located SpecType))])
-> GhcSpecSig -> [(Var, 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]
hsCs  (CGInfo -> [SubC])
-> StateT CGInfo Identity CGInfo -> StateT CGInfo Identity [SubC]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT CGInfo Identity CGInfo
forall s (m :: * -> *). MonadState s m => m s
get
  [WfC]
hws <- CGInfo -> [WfC]
hsWfs (CGInfo -> [WfC])
-> StateT CGInfo Identity CGInfo -> StateT CGInfo Identity [WfC]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT CGInfo Identity CGInfo
forall s (m :: * -> *). MonadState s m => m s
get
  [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)
mapM SubC -> StateT CGInfo Identity [FixSubC]
splitC [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)
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 :: SEnv Sort
fEnv     = FEnv -> SEnv Sort
feEnv (CGEnv -> FEnv
fenv CGEnv
γ)
                     , cgLits :: SEnv Sort
cgLits   = CGEnv -> SEnv Sort
litEnv   CGEnv
γ
                     , cgConsts :: SEnv Sort
cgConsts = (CGInfo -> SEnv Sort
cgConsts CGInfo
st) SEnv Sort -> SEnv Sort -> SEnv Sort
forall a. Monoid a => a -> a -> a
`mappend` (CGEnv -> SEnv Sort
constEnv CGEnv
γ)
                     , fixCs :: [FixSubC]
fixCs    = [FixSubC]
fcs
                     , fixWfs :: [FixWfC]
fixWfs   = [FixWfC]
fws }



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

consClass :: CGEnv -> (Var, MethodType LocSpecType) -> CG ()
consClass :: CGEnv -> (Var, MethodType (Located SpecType)) -> State CGInfo ()
consClass CGEnv
γ (Var
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 -> String -> 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)) (String
"cconsClass for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Var -> String
forall a. Outputable a => a -> String
GM.showPpr Var
x)
consClass CGEnv
_ (Var, MethodType (Located SpecType))
_ 
  = () -> State CGInfo ()
forall (m :: * -> *) a. Monad m => a -> m a
return () 

--------------------------------------------------------------------------------
-- | TERMINATION TYPE ----------------------------------------------------------
--------------------------------------------------------------------------------
makeDecrIndex :: (Var, Template SpecType, [Var]) -> CG [Int]
makeDecrIndex :: (Var, Template SpecType, [Var]) -> CG [Int]
makeDecrIndex (Var
x, Assumed SpecType
t, [Var]
args)
  = do Either (TError Any) [Int]
dindex <- Var -> SpecType -> [Var] -> CG (Either (TError Any) [Int])
forall t. Var -> SpecType -> [Var] -> CG (Either (TError t) [Int])
makeDecrIndexTy Var
x SpecType
t [Var]
args
       case Either (TError Any) [Int]
dindex of
         Left TError Any
_  -> [Int] -> CG [Int]
forall (m :: * -> *) a. Monad m => a -> m a
return []
         Right [Int]
i -> [Int] -> CG [Int]
forall (m :: * -> *) a. Monad m => a -> m a
return [Int]
i
makeDecrIndex (Var
x, Asserted SpecType
t, [Var]
args)
  = do Either (TError SpecType) [Int]
dindex <- Var -> SpecType -> [Var] -> CG (Either (TError SpecType) [Int])
forall t. Var -> SpecType -> [Var] -> CG (Either (TError t) [Int])
makeDecrIndexTy Var
x SpecType
t [Var]
args
       case Either (TError SpecType) [Int]
dindex of
         Left TError SpecType
msg -> TError SpecType -> State CGInfo ()
addWarning TError SpecType
msg State CGInfo () -> CG [Int] -> CG [Int]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [Int] -> CG [Int]
forall (m :: * -> *) a. Monad m => a -> m a
return []
         Right [Int]
i  -> [Int] -> CG [Int]
forall (m :: * -> *) a. Monad m => a -> m a
return [Int]
i
makeDecrIndex (Var, Template SpecType, [Var])
_ = [Int] -> CG [Int]
forall (m :: * -> *) a. Monad m => a -> m a
return []

makeDecrIndexTy :: Var -> SpecType -> [Var] -> CG (Either (TError t) [Int])
makeDecrIndexTy :: Var -> SpecType -> [Var] -> CG (Either (TError t) [Int])
makeDecrIndexTy Var
x SpecType
t [Var]
args
  = do [(Var, [Int])]
spDecr <- CGInfo -> [(Var, [Int])]
specDecr (CGInfo -> [(Var, [Int])])
-> StateT CGInfo Identity CGInfo
-> StateT CGInfo Identity [(Var, [Int])]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT CGInfo Identity CGInfo
forall s (m :: * -> *). MonadState s m => m s
get
       HashSet TyCon
autosz <- CGInfo -> HashSet TyCon
autoSize (CGInfo -> HashSet TyCon)
-> StateT CGInfo Identity CGInfo
-> StateT CGInfo Identity (HashSet TyCon)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT CGInfo Identity CGInfo
forall s (m :: * -> *). MonadState s m => m s
get
       Maybe [Int]
hint   <- HashSet TyCon -> Maybe [Int] -> CG (Maybe [Int])
checkHint' HashSet TyCon
autosz (Var -> [(Var, [Int])] -> Maybe [Int]
forall a b. Eq a => a -> [(a, b)] -> Maybe b
L.lookup Var
x [(Var, [Int])]
spDecr)
       case HashSet TyCon -> Maybe Int
dindex HashSet TyCon
autosz of
         Maybe Int
Nothing -> Either (TError t) [Int] -> CG (Either (TError t) [Int])
forall (m :: * -> *) a. Monad m => a -> m a
return (Either (TError t) [Int] -> CG (Either (TError t) [Int]))
-> Either (TError t) [Int] -> CG (Either (TError t) [Int])
forall a b. (a -> b) -> a -> b
$ TError t -> Either (TError t) [Int]
forall a b. a -> Either a b
Left TError t
forall t. TError t
msg
         Just Int
i  -> Either (TError t) [Int] -> CG (Either (TError t) [Int])
forall (m :: * -> *) a. Monad m => a -> m a
return (Either (TError t) [Int] -> CG (Either (TError t) [Int]))
-> Either (TError t) [Int] -> CG (Either (TError t) [Int])
forall a b. (a -> b) -> a -> b
$ [Int] -> Either (TError t) [Int]
forall a b. b -> Either a b
Right ([Int] -> Either (TError t) [Int])
-> [Int] -> Either (TError t) [Int]
forall a b. (a -> b) -> a -> b
$ [Int] -> Maybe [Int] -> [Int]
forall a. a -> Maybe a -> a
fromMaybe [Int
i] Maybe [Int]
hint
    where
       ts :: [SpecType]
ts         = RTypeRep RTyCon RTyVar RReft -> [SpecType]
forall c tv r. RTypeRep c tv r -> [RType c tv r]
ty_args RTypeRep RTyCon RTyVar RReft
trep
       tvs :: [(SpecType, Var)]
tvs        = [SpecType] -> [Var] -> [(SpecType, Var)]
forall a b. [a] -> [b] -> [(a, b)]
zip [SpecType]
ts [Var]
args
       checkHint' :: HashSet TyCon -> Maybe [Int] -> CG (Maybe [Int])
checkHint' = \HashSet TyCon
autosz -> Var
-> [SpecType]
-> (SpecType -> Bool)
-> Maybe [Int]
-> CG (Maybe [Int])
forall a a1.
(NamedThing a, PPrint a, PPrint a1) =>
a -> [a1] -> (a1 -> Bool) -> Maybe [Int] -> CG (Maybe [Int])
checkHint Var
x [SpecType]
ts (HashSet TyCon -> [RTyVar] -> SpecType -> Bool
isDecreasing HashSet TyCon
autosz [RTyVar]
cenv)
       dindex :: HashSet TyCon -> Maybe Int
dindex     = \HashSet TyCon
autosz -> ((SpecType, Var) -> Bool) -> [(SpecType, Var)] -> Maybe Int
forall a. (a -> Bool) -> [a] -> Maybe Int
L.findIndex (HashSet TyCon -> (SpecType, Var) -> Bool
p HashSet TyCon
autosz) [(SpecType, Var)]
tvs
       p :: HashSet TyCon -> (SpecType, Var) -> Bool
p HashSet TyCon
autosz (SpecType
t, Var
v) = HashSet TyCon -> [RTyVar] -> SpecType -> Bool
isDecreasing HashSet TyCon
autosz [RTyVar]
cenv SpecType
t Bool -> Bool -> Bool
&& Bool -> Bool
not (Var -> Bool
isIdTRecBound Var
v)
       msg :: TError t
msg        = SrcSpan -> [Doc] -> Doc -> TError t
forall t. SrcSpan -> [Doc] -> Doc -> TError t
ErrTermin (Var -> SrcSpan
forall a. NamedThing a => a -> SrcSpan
getSrcSpan Var
x) [Var -> Doc
forall a. PPrint a => a -> Doc
F.pprint Var
x] (String -> Doc
text String
"No decreasing parameter")
       cenv :: [RTyVar]
cenv       = [SpecType] -> [RTyVar]
forall (t :: * -> *) c b t1.
(Foldable t, TyConable c) =>
t (RType c b t1) -> [b]
makeNumEnv [SpecType]
ts
       trep :: RTypeRep RTyCon RTyVar RReft
trep       = SpecType -> RTypeRep RTyCon RTyVar RReft
forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep (SpecType -> RTypeRep RTyCon RTyVar RReft)
-> SpecType -> RTypeRep RTyCon RTyVar RReft
forall a b. (a -> b) -> a -> b
$ SpecType -> SpecType
forall c tv r. RType c tv r -> RType c tv r
unOCons SpecType
t


recType :: F.Symbolic a
        => S.HashSet TyCon
        -> (([a], [Int]), (t, [Int], SpecType))
        -> SpecType
recType :: HashSet TyCon -> (([a], [Int]), (t, [Int], SpecType)) -> SpecType
recType HashSet TyCon
_ (([a]
_, []), (t
_, [], SpecType
t))
  = SpecType
t

recType HashSet TyCon
autoenv (([a]
vs, [Int]
indexc), (t
_, [Int]
index, SpecType
t))
  = HashSet TyCon
-> SpecType -> [a] -> [(Symbol, SpecType)] -> [Int] -> SpecType
forall a1 a.
(Enum a1, Eq a1, Num a1, Symbolic a) =>
HashSet TyCon
-> SpecType -> [a] -> [(Symbol, SpecType)] -> [a1] -> SpecType
makeRecType HashSet TyCon
autoenv SpecType
t [a]
v [(Symbol, SpecType)]
dxt [Int]
index
  where v :: [a]
v    = ([a]
vs [a] -> Int -> a
forall a. [a] -> Int -> a
!!)  (Int -> a) -> [Int] -> [a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Int]
indexc
        dxt :: [(Symbol, SpecType)]
dxt  = ([(Symbol, SpecType)]
xts [(Symbol, SpecType)] -> Int -> (Symbol, SpecType)
forall a. [a] -> Int -> a
!!) (Int -> (Symbol, SpecType)) -> [Int] -> [(Symbol, SpecType)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Int]
index
        xts :: [(Symbol, SpecType)]
xts  = [Symbol] -> [SpecType] -> [(Symbol, SpecType)]
forall a b. [a] -> [b] -> [(a, b)]
zip (RTypeRep RTyCon RTyVar RReft -> [Symbol]
forall c tv r. RTypeRep c tv r -> [Symbol]
ty_binds RTypeRep RTyCon RTyVar RReft
trep) (RTypeRep RTyCon RTyVar RReft -> [SpecType]
forall c tv r. RTypeRep c tv r -> [RType c tv r]
ty_args RTypeRep RTyCon RTyVar RReft
trep)
        trep :: RTypeRep RTyCon RTyVar RReft
trep = SpecType -> RTypeRep RTyCon RTyVar RReft
forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep (SpecType -> RTypeRep RTyCon RTyVar RReft)
-> SpecType -> RTypeRep RTyCon RTyVar RReft
forall a b. (a -> b) -> a -> b
$ SpecType -> SpecType
forall c tv r. RType c tv r -> RType c tv r
unOCons SpecType
t

checkIndex :: (NamedThing t, PPrint t, PPrint a)
           => (t, [a], Template (RType c tv r), [Int])
           -> CG [Maybe (RType c tv r)]
checkIndex :: (t, [a], Template (RType c tv r), [Int])
-> CG [Maybe (RType c tv r)]
checkIndex (t
x, [a]
vs, Template (RType c tv r)
t, [Int]
index)
  = do (Int -> StateT CGInfo Identity (Maybe a))
-> [Int] -> State CGInfo ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (TError SpecType -> [a] -> Int -> StateT CGInfo Identity (Maybe a)
forall a. TError SpecType -> [a] -> Int -> CG (Maybe a)
safeLogIndex TError SpecType
forall t. TError t
msg1 [a]
vs) [Int]
index
       (Int -> StateT CGInfo Identity (Maybe (RType c tv r)))
-> [Int] -> CG [Maybe (RType c tv r)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM  (TError SpecType
-> [RType c tv r]
-> Int
-> StateT CGInfo Identity (Maybe (RType c tv r))
forall a. TError SpecType -> [a] -> Int -> CG (Maybe a)
safeLogIndex TError SpecType
forall t. TError t
msg2 [RType c tv r]
ts) [Int]
index
    where
       loc :: SrcSpan
loc   = t -> SrcSpan
forall a. NamedThing a => a -> SrcSpan
getSrcSpan t
x
       ts :: [RType c tv r]
ts    = RTypeRep c tv r -> [RType c tv r]
forall c tv r. RTypeRep c tv r -> [RType c tv r]
ty_args (RTypeRep c tv r -> [RType c tv r])
-> RTypeRep c tv r -> [RType c tv r]
forall a b. (a -> b) -> a -> b
$ RType c tv r -> RTypeRep c tv r
forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep (RType c tv r -> RTypeRep c tv r)
-> RType c tv r -> RTypeRep c tv r
forall a b. (a -> b) -> a -> b
$ RType c tv r -> RType c tv r
forall c tv r. RType c tv r -> RType c tv r
unOCons (RType c tv r -> RType c tv r) -> RType c tv r -> RType c tv r
forall a b. (a -> b) -> a -> b
$ Template (RType c tv r) -> RType c tv r
forall t. Template t -> t
unTemplate Template (RType c tv r)
t
       msg1 :: TError t
msg1  = SrcSpan -> [Doc] -> Doc -> TError t
forall t. SrcSpan -> [Doc] -> Doc -> TError t
ErrTermin SrcSpan
loc [Doc
xd] (Doc
"No decreasing" Doc -> Doc -> Doc
<+> [Int] -> Doc
forall a. PPrint a => a -> Doc
F.pprint [Int]
index Doc -> Doc -> Doc
<-> Doc
"-th argument on" Doc -> Doc -> Doc
<+> Doc
xd Doc -> Doc -> Doc
<+> Doc
"with" Doc -> Doc -> Doc
<+> ([a] -> Doc
forall a. PPrint a => a -> Doc
F.pprint [a]
vs))
       msg2 :: TError t
msg2  = SrcSpan -> [Doc] -> Doc -> TError t
forall t. SrcSpan -> [Doc] -> Doc -> TError t
ErrTermin SrcSpan
loc [Doc
xd] Doc
"No decreasing parameter"
       xd :: Doc
xd    = t -> Doc
forall a. PPrint a => a -> Doc
F.pprint t
x

makeRecType :: (Enum a1, Eq a1, Num a1, F.Symbolic a)
            => S.HashSet TyCon
            -> SpecType
            -> [a]
            -> [(F.Symbol, SpecType)]
            -> [a1]
            -> SpecType
makeRecType :: HashSet TyCon
-> SpecType -> [a] -> [(Symbol, SpecType)] -> [a1] -> SpecType
makeRecType HashSet TyCon
autoenv SpecType
t [a]
vs [(Symbol, SpecType)]
dxs [a1]
is
  = SpecType -> SpecType -> SpecType
forall c tv r. RType c tv r -> RType c tv r -> RType c tv r
mergecondition SpecType
t (SpecType -> SpecType) -> SpecType -> SpecType
forall a b. (a -> b) -> a -> b
$ RTypeRep RTyCon RTyVar RReft -> SpecType
forall c tv r. RTypeRep c tv r -> RType c tv r
fromRTypeRep (RTypeRep RTyCon RTyVar RReft -> SpecType)
-> RTypeRep RTyCon RTyVar RReft -> SpecType
forall a b. (a -> b) -> a -> b
$ RTypeRep RTyCon RTyVar RReft
trep {ty_binds :: [Symbol]
ty_binds = [Symbol]
xs', ty_args :: [SpecType]
ty_args = [SpecType]
ts'}
  where
    ([Symbol]
xs', [SpecType]
ts') = [(Symbol, SpecType)] -> ([Symbol], [SpecType])
forall a b. [(a, b)] -> ([a], [b])
unzip ([(Symbol, SpecType)] -> ([Symbol], [SpecType]))
-> [(Symbol, SpecType)] -> ([Symbol], [SpecType])
forall a b. (a -> b) -> a -> b
$ a1
-> (Symbol, SpecType)
-> [(Symbol, SpecType)]
-> [(Symbol, SpecType)]
forall a t. (Enum a, Eq a, Num a) => a -> t -> [t] -> [t]
replaceN ([a1] -> a1
forall a. [a] -> a
last [a1]
is) (String -> Either (Symbol, SpecType) String -> (Symbol, SpecType)
forall a b. String -> Either a b -> a
safeFromLeft String
"makeRecType" (Either (Symbol, SpecType) String -> (Symbol, SpecType))
-> Either (Symbol, SpecType) String -> (Symbol, SpecType)
forall a b. (a -> b) -> a -> b
$ HashSet TyCon
-> [(a, (Symbol, SpecType))] -> Either (Symbol, SpecType) String
forall a t.
Symbolic a =>
HashSet TyCon
-> [(a, (Symbol, RType RTyCon t RReft))]
-> Either (Symbol, RType RTyCon t RReft) String
makeDecrType HashSet TyCon
autoenv [(a, (Symbol, SpecType))]
vdxs) [(Symbol, SpecType)]
xts
    vdxs :: [(a, (Symbol, SpecType))]
vdxs       = [a] -> [(Symbol, SpecType)] -> [(a, (Symbol, SpecType))]
forall a b. [a] -> [b] -> [(a, b)]
zip [a]
vs [(Symbol, SpecType)]
dxs
    xts :: [(Symbol, SpecType)]
xts        = [Symbol] -> [SpecType] -> [(Symbol, SpecType)]
forall a b. [a] -> [b] -> [(a, b)]
zip (RTypeRep RTyCon RTyVar RReft -> [Symbol]
forall c tv r. RTypeRep c tv r -> [Symbol]
ty_binds RTypeRep RTyCon RTyVar RReft
trep) (RTypeRep RTyCon RTyVar RReft -> [SpecType]
forall c tv r. RTypeRep c tv r -> [RType c tv r]
ty_args RTypeRep RTyCon RTyVar RReft
trep)
    trep :: RTypeRep RTyCon RTyVar RReft
trep       = SpecType -> RTypeRep RTyCon RTyVar RReft
forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep (SpecType -> RTypeRep RTyCon RTyVar RReft)
-> SpecType -> RTypeRep RTyCon RTyVar RReft
forall a b. (a -> b) -> a -> b
$ SpecType -> SpecType
forall c tv r. RType c tv r -> RType c tv r
unOCons SpecType
t

unOCons :: RType c tv r -> RType c tv r
unOCons :: RType c tv r -> RType c tv r
unOCons (RAllT RTVU c tv
v 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
v (RType c tv r -> RType c tv r
forall c tv r. RType c tv r -> RType c tv r
unOCons RType c tv r
t) r
r 
unOCons (RAllP PVU c tv
p RType c tv r
t)        = PVU c tv -> RType c tv r -> RType c tv r
forall c tv r. PVU c tv -> RType c tv r -> RType c tv r
RAllP PVU c tv
p (RType c tv r -> RType c tv r) -> RType c tv r -> RType c tv r
forall a b. (a -> b) -> a -> b
$ RType c tv r -> RType c tv r
forall c tv r. RType c tv r -> RType c tv r
unOCons RType c tv r
t
unOCons (RFun Symbol
x RType c tv r
tx RType c tv r
t r
r)    = Symbol -> RType c tv r -> RType c tv r -> r -> RType c tv r
forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
x (RType c tv r -> RType c tv r
forall c tv r. RType c tv r -> RType c tv r
unOCons RType c tv r
tx) (RType c tv r -> RType c tv r
forall c tv r. RType c tv r -> RType c tv r
unOCons RType c tv r
t) r
r
unOCons (RRTy [(Symbol, RType c tv r)]
_ r
_ Oblig
OCons RType c tv r
t) = RType c tv r -> RType c tv r
forall c tv r. RType c tv r -> RType c tv r
unOCons RType c tv r
t
unOCons RType c tv r
t                  = RType c tv r
t

mergecondition :: RType c tv r -> RType c tv r -> RType c tv r
mergecondition :: RType c tv r -> RType c tv r -> RType c tv r
mergecondition (RAllT RTVU c tv
_ RType c tv r
t1 r
_) (RAllT RTVU c tv
v RType c tv r
t2 r
r2)          = 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
v (RType c tv r -> RType c tv r -> RType c tv r
forall c tv r. RType c tv r -> RType c tv r -> RType c tv r
mergecondition RType c tv r
t1 RType c tv r
t2) r
r2 
mergecondition (RAllP PVU c tv
_ RType c tv r
t1) (RAllP PVU c tv
p RType c tv r
t2)               = PVU c tv -> RType c tv r -> RType c tv r
forall c tv r. PVU c tv -> RType c tv r -> RType c tv r
RAllP PVU c tv
p (RType c tv r -> RType c tv r -> RType c tv r
forall c tv r. RType c tv r -> RType c tv r -> RType c tv r
mergecondition RType c tv r
t1 RType c tv r
t2)
mergecondition (RRTy [(Symbol, RType c tv r)]
xts r
r Oblig
OCons RType c tv r
t1) RType c tv r
t2                = [(Symbol, RType c tv r)]
-> r -> Oblig -> RType c tv r -> RType c tv r
forall c tv r.
[(Symbol, RType c tv r)]
-> r -> Oblig -> RType c tv r -> RType c tv r
RRTy [(Symbol, RType c tv r)]
xts r
r Oblig
OCons (RType c tv r -> RType c tv r -> RType c tv r
forall c tv r. RType c tv r -> RType c tv r -> RType c tv r
mergecondition RType c tv r
t1 RType c tv r
t2)
mergecondition (RFun Symbol
_ RType c tv r
t11 RType c tv r
t12 r
_) (RFun Symbol
x2 RType c tv r
t21 RType c tv r
t22 r
r2) = Symbol -> RType c tv r -> RType c tv r -> r -> RType c tv r
forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
x2 (RType c tv r -> RType c tv r -> RType c tv r
forall c tv r. RType c tv r -> RType c tv r -> RType c tv r
mergecondition RType c tv r
t11 RType c tv r
t21) (RType c tv r -> RType c tv r -> RType c tv r
forall c tv r. RType c tv r -> RType c tv r -> RType c tv r
mergecondition RType c tv r
t12 RType c tv r
t22) r
r2
mergecondition RType c tv r
_ RType c tv r
t                                     = RType c tv r
t

safeLogIndex :: Error -> [a] -> Int -> CG (Maybe a)
safeLogIndex :: TError SpecType -> [a] -> Int -> CG (Maybe a)
safeLogIndex TError SpecType
err [a]
ls Int
n
  | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
ls = TError SpecType -> State CGInfo ()
addWarning TError SpecType
err State CGInfo () -> CG (Maybe a) -> CG (Maybe a)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Maybe a -> CG (Maybe a)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe a
forall a. Maybe a
Nothing
  | Bool
otherwise      = Maybe a -> CG (Maybe a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe a -> CG (Maybe a)) -> Maybe a -> CG (Maybe a)
forall a b. (a -> b) -> a -> b
$ a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> a -> Maybe a
forall a b. (a -> b) -> a -> b
$ [a]
ls [a] -> Int -> a
forall a. [a] -> Int -> a
!! Int
n

checkHint :: (NamedThing a, PPrint a, PPrint a1)
          => a -> [a1] -> (a1 -> Bool) -> Maybe [Int] -> CG (Maybe [Int])
checkHint :: a -> [a1] -> (a1 -> Bool) -> Maybe [Int] -> CG (Maybe [Int])
checkHint a
_ [a1]
_ a1 -> Bool
_ Maybe [Int]
Nothing
  = Maybe [Int] -> CG (Maybe [Int])
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe [Int]
forall a. Maybe a
Nothing

checkHint a
x [a1]
_ a1 -> Bool
_ (Just [Int]
ns) | [Int] -> [Int]
forall a. Ord a => [a] -> [a]
L.sort [Int]
ns [Int] -> [Int] -> Bool
forall a. Eq a => a -> a -> Bool
/= [Int]
ns
  = TError SpecType -> State CGInfo ()
addWarning (SrcSpan -> [Doc] -> Doc -> TError SpecType
forall t. SrcSpan -> [Doc] -> Doc -> TError t
ErrTermin SrcSpan
loc [Doc
dx] (String -> Doc
text String
"The hints should be increasing")) State CGInfo () -> CG (Maybe [Int]) -> CG (Maybe [Int])
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Maybe [Int] -> CG (Maybe [Int])
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe [Int]
forall a. Maybe a
Nothing
  where
    loc :: SrcSpan
loc = a -> SrcSpan
forall a. NamedThing a => a -> SrcSpan
getSrcSpan a
x
    dx :: Doc
dx  = a -> Doc
forall a. PPrint a => a -> Doc
F.pprint a
x

checkHint a
x [a1]
ts a1 -> Bool
f (Just [Int]
ns)
  = ((Int -> StateT CGInfo Identity (Maybe Int))
-> [Int] -> StateT CGInfo Identity [Maybe Int]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (a
-> [a1]
-> (a1 -> Bool)
-> Int
-> StateT CGInfo Identity (Maybe Int)
forall a a1.
(NamedThing a, PPrint a, PPrint a1) =>
a
-> [a1]
-> (a1 -> Bool)
-> Int
-> StateT CGInfo Identity (Maybe Int)
checkValidHint a
x [a1]
ts a1 -> Bool
f) [Int]
ns) StateT CGInfo Identity [Maybe Int]
-> ([Maybe Int] -> CG (Maybe [Int])) -> CG (Maybe [Int])
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (Maybe [Int] -> CG (Maybe [Int])
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe [Int] -> CG (Maybe [Int]))
-> ([Maybe Int] -> Maybe [Int]) -> [Maybe Int] -> CG (Maybe [Int])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Int] -> Maybe [Int]
forall a. a -> Maybe a
Just ([Int] -> Maybe [Int])
-> ([Maybe Int] -> [Int]) -> [Maybe Int] -> Maybe [Int]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Maybe Int] -> [Int]
forall a. [Maybe a] -> [a]
catMaybes)

checkValidHint :: (NamedThing a, PPrint a, PPrint a1)
               => a -> [a1] -> (a1 -> Bool) -> Int -> CG (Maybe Int)
checkValidHint :: a
-> [a1]
-> (a1 -> Bool)
-> Int
-> StateT CGInfo Identity (Maybe Int)
checkValidHint a
x [a1]
ts a1 -> Bool
f Int
n
  | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0 Bool -> Bool -> Bool
|| Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= [a1] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a1]
ts = TError SpecType -> State CGInfo ()
addWarning TError SpecType
forall t. TError t
err State CGInfo ()
-> StateT CGInfo Identity (Maybe Int)
-> StateT CGInfo Identity (Maybe Int)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Maybe Int -> StateT CGInfo Identity (Maybe Int)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Int
forall a. Maybe a
Nothing
  | a1 -> Bool
f ([a1]
ts [a1] -> Int -> a1
forall a. [a] -> Int -> a
L.!! Int
n)           = Maybe Int -> StateT CGInfo Identity (Maybe Int)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Int -> StateT CGInfo Identity (Maybe Int))
-> Maybe Int -> StateT CGInfo Identity (Maybe Int)
forall a b. (a -> b) -> a -> b
$ Int -> Maybe Int
forall a. a -> Maybe a
Just Int
n
  | Bool
otherwise               = TError SpecType -> State CGInfo ()
addWarning TError SpecType
forall t. TError t
err State CGInfo ()
-> StateT CGInfo Identity (Maybe Int)
-> StateT CGInfo Identity (Maybe Int)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Maybe Int -> StateT CGInfo Identity (Maybe Int)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Int
forall a. Maybe a
Nothing
  where
    err :: TError t
err = SrcSpan -> [Doc] -> Doc -> TError t
forall t. SrcSpan -> [Doc] -> Doc -> TError t
ErrTermin SrcSpan
loc [Doc
xd] ([Doc] -> Doc
vcat [ Doc
"Invalid Hint" Doc -> Doc -> Doc
<+> Int -> Doc
forall a. PPrint a => a -> Doc
F.pprint (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Doc -> Doc -> Doc
<+> Doc
"for" Doc -> Doc -> Doc
<+> Doc
xd
                                   , Doc
"in"
                                   , [a1] -> Doc
forall a. PPrint a => a -> Doc
F.pprint [a1]
ts ])
    loc :: SrcSpan
loc = a -> SrcSpan
forall a. NamedThing a => a -> SrcSpan
getSrcSpan a
x
    xd :: Doc
xd  = a -> Doc
forall a. PPrint a => a -> Doc
F.pprint a
x

--------------------------------------------------------------------------------
consCBLet :: CGEnv -> CoreBind -> CG CGEnv
--------------------------------------------------------------------------------
consCBLet :: CGEnv -> CoreBind -> CG CGEnv
consCBLet CGEnv
γ CoreBind
cb = do
  Bool
oldtcheck <- CGInfo -> Bool
tcheck (CGInfo -> Bool)
-> StateT CGInfo Identity CGInfo -> StateT CGInfo Identity Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT CGInfo Identity CGInfo
forall s (m :: * -> *). MonadState s m => m s
get
  Bool
isStr     <- Config -> CoreBind -> StateT CGInfo Identity Bool
doTermCheck (CGEnv -> Config
forall t. HasConfig t => t -> Config
getConfig CGEnv
γ) CoreBind
cb
  -- TODO: yuck.
  (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 :: Bool
tcheck = Bool
oldtcheck Bool -> Bool -> Bool
&& Bool
isStr }
  CGEnv
γ' <- Bool -> Bool -> CGEnv -> CoreBind -> CG CGEnv
consCB (Bool
oldtcheck Bool -> Bool -> Bool
&& Bool
isStr) 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 :: Bool
tcheck = Bool
oldtcheck}
  CGEnv -> CG CGEnv
forall (m :: * -> *) a. Monad m => a -> m a
return CGEnv
γ'

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

consCBTop Config
_ TargetInfo
_ CGEnv
γ CoreBind
cb
  = do Bool
oldtcheck <- CGInfo -> Bool
tcheck (CGInfo -> Bool)
-> StateT CGInfo Identity CGInfo -> StateT CGInfo Identity Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT CGInfo Identity CGInfo
forall s (m :: * -> *). MonadState s m => m s
get
       -- lazyVars  <- specLazy <$> get
       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 :: Bool
tcheck = Bool
oldtcheck Bool -> Bool -> Bool
&& Bool
isStr}
       -- remove invariants that came from the cb definition
       let (CGEnv
γ', RTyConInv
i) = CGEnv -> CoreBind -> (CGEnv, RTyConInv)
removeInvariant CGEnv
γ CoreBind
cb                 --- DIFF
       CGEnv
γ'' <- Bool -> Bool -> CGEnv -> CoreBind -> CG CGEnv
consCB (Bool
oldtcheck Bool -> Bool -> Bool
&& Bool
isStr) Bool
isStr (CGEnv
γ'{cgVar :: Maybe Var
cgVar = CoreBind -> Maybe Var
forall a. Bind a -> Maybe a
topBind CoreBind
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 :: Bool
tcheck = Bool
oldtcheck}
       CGEnv -> CG CGEnv
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                    --- DIFF
    where
      topBind :: Bind a -> Maybe a
topBind (NonRec a
v Expr a
_)  = a -> Maybe a
forall a. a -> Maybe a
Just a
v
      topBind (Rec [(a
v,Expr a
_)]) = a -> Maybe a
forall a. a -> Maybe a
Just a
v
      topBind Bind a
_             = Maybe a
forall a. Maybe a
Nothing

trustVar :: Config -> TargetInfo -> Var -> Bool
trustVar :: Config -> TargetInfo -> Var -> Bool
trustVar Config
cfg TargetInfo
info Var
x = Bool -> Bool
not (Config -> Bool
checkDerived Config
cfg) Bool -> Bool -> Bool
&& TargetSrc -> Var -> Bool
derivedVar (TargetInfo -> TargetSrc
giSrc TargetInfo
info) Var
x

derivedVar :: TargetSrc -> Var -> Bool
derivedVar :: TargetSrc -> Var -> Bool
derivedVar TargetSrc
src Var
x = Var -> HashSet Var -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member Var
x (TargetSrc -> HashSet Var
giDerVars TargetSrc
src)

doTermCheck :: Config -> Bind Var -> CG Bool
doTermCheck :: Config -> CoreBind -> StateT CGInfo Identity Bool
doTermCheck Config
cfg CoreBind
bind = do 
  HashSet Var
lazyVs    <- CGInfo -> HashSet Var
specLazy   (CGInfo -> HashSet Var)
-> StateT CGInfo Identity CGInfo
-> StateT CGInfo Identity (HashSet Var)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT CGInfo Identity CGInfo
forall s (m :: * -> *). MonadState s m => m s
get 
  HashSet Var
termVs    <- CGInfo -> HashSet Var
specTmVars (CGInfo -> HashSet Var)
-> StateT CGInfo Identity CGInfo
-> StateT CGInfo Identity (HashSet Var)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT CGInfo Identity CGInfo
forall s (m :: * -> *). MonadState s m => m s
get
  let skip :: Bool
skip   = (Var -> Bool) -> [Var] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\Var
x -> Var -> HashSet Var -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member Var
x HashSet Var
lazyVs Bool -> Bool -> Bool
|| Var -> Bool
forall a. Symbolic a => a -> Bool
GM.isInternal Var
x) [Var]
xs
  let chk :: Bool
chk    = Bool -> Bool
not (Config -> Bool
forall a. HasConfig a => a -> Bool
structuralTerm Config
cfg) Bool -> Bool -> Bool
|| (Var -> Bool) -> [Var] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\Var
x -> Var -> HashSet Var -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member Var
x HashSet Var
termVs) [Var]
xs
  Bool -> StateT CGInfo Identity Bool
forall (m :: * -> *) a. Monad m => a -> m a
return     (Bool -> StateT CGInfo Identity Bool)
-> Bool -> StateT CGInfo Identity Bool
forall a b. (a -> b) -> a -> b
$ Bool
chk Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
skip
  where 
    xs :: [Var]
xs       = CoreBind -> [Var]
forall b. Bind b -> [b]
bindersOf CoreBind
bind

-- nonStructTerm && not skip

-- RJ: AAAAAAARGHHH!!!!!! THIS CODE IS HORRIBLE!!!!!!!!!
consCBSizedTys :: CGEnv -> [(Var, CoreExpr)] -> CG CGEnv
consCBSizedTys :: CGEnv -> [(Var, CoreExpr)] -> CG CGEnv
consCBSizedTys CGEnv
γ [(Var, CoreExpr)]
xes
  = do [(Var, CoreExpr, Template SpecType)]
xets     <- [(Var, CoreExpr)]
-> ((Var, CoreExpr)
    -> StateT CGInfo Identity (Var, CoreExpr, Template SpecType))
-> StateT CGInfo Identity [(Var, CoreExpr, Template SpecType)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Var, CoreExpr)]
xes (((Var, CoreExpr)
  -> StateT CGInfo Identity (Var, CoreExpr, Template SpecType))
 -> StateT CGInfo Identity [(Var, CoreExpr, Template SpecType)])
-> ((Var, CoreExpr)
    -> StateT CGInfo Identity (Var, CoreExpr, Template SpecType))
-> StateT CGInfo Identity [(Var, CoreExpr, Template SpecType)]
forall a b. (a -> b) -> a -> b
$ \(Var
x, CoreExpr
e) -> (Template SpecType -> (Var, CoreExpr, Template SpecType))
-> StateT CGInfo Identity (Template SpecType)
-> StateT CGInfo Identity (Var, CoreExpr, Template SpecType)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (Var
x, CoreExpr
e,) (CGEnv
-> (Var, Maybe CoreExpr)
-> StateT CGInfo Identity (Template SpecType)
varTemplate CGEnv
γ (Var
x, CoreExpr -> Maybe CoreExpr
forall a. a -> Maybe a
Just CoreExpr
e))
       HashSet TyCon
autoenv  <- CGInfo -> HashSet TyCon
autoSize (CGInfo -> HashSet TyCon)
-> StateT CGInfo Identity CGInfo
-> StateT CGInfo Identity (HashSet TyCon)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT CGInfo Identity CGInfo
forall s (m :: * -> *). MonadState s m => m s
get
       [Template SpecType]
ts       <- (Template SpecType -> StateT CGInfo Identity (Template SpecType))
-> [Template SpecType]
-> StateT CGInfo Identity [Template SpecType]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((SpecType -> CG SpecType)
-> Template SpecType -> StateT CGInfo Identity (Template SpecType)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
T.mapM SpecType -> CG SpecType
forall (m :: * -> *). FreshM m => SpecType -> m SpecType
refreshArgs) ([Template SpecType] -> StateT CGInfo Identity [Template SpecType])
-> [Template SpecType]
-> StateT CGInfo Identity [Template SpecType]
forall a b. (a -> b) -> a -> b
$ ((Var, CoreExpr, Template SpecType) -> Template SpecType
forall a b c. (a, b, c) -> c
thd3 ((Var, CoreExpr, Template SpecType) -> Template SpecType)
-> [(Var, CoreExpr, Template SpecType)] -> [Template SpecType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Var, CoreExpr, Template SpecType)]
xets)
       let vs :: [[Var]]
vs    = (Template SpecType -> CoreExpr -> [Var])
-> [Template SpecType] -> [CoreExpr] -> [[Var]]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Template SpecType -> CoreExpr -> [Var]
forall c tv r. Template (RType c tv r) -> CoreExpr -> [Var]
collectArgs [Template SpecType]
ts [CoreExpr]
es
       [[Int]]
is       <- ((Var, Template SpecType, [Var]) -> CG [Int])
-> [(Var, Template SpecType, [Var])]
-> StateT CGInfo Identity [[Int]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Var, Template SpecType, [Var]) -> CG [Int]
makeDecrIndex ([Var]
-> [Template SpecType]
-> [[Var]]
-> [(Var, Template SpecType, [Var])]
forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
zip3 [Var]
xs [Template SpecType]
ts [[Var]]
vs) StateT CGInfo Identity [[Int]]
-> ([[Int]] -> StateT CGInfo Identity [[Int]])
-> StateT CGInfo Identity [[Int]]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [[Int]] -> StateT CGInfo Identity [[Int]]
forall (t :: * -> *) a.
Foldable t =>
[t a] -> StateT CGInfo Identity [t a]
checkSameLens
       let xeets :: [[(([Var], [Int]), (Var, [Int], SpecType))]]
xeets = (\([Var], [Int])
vis -> [(([Var], [Int])
vis, (Var, [Int], SpecType)
x) | (Var, [Int], SpecType)
x <- [Var] -> [[Int]] -> [SpecType] -> [(Var, [Int], SpecType)]
forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
zip3 [Var]
xs [[Int]]
is ([SpecType] -> [(Var, [Int], SpecType)])
-> [SpecType] -> [(Var, [Int], SpecType)]
forall a b. (a -> b) -> a -> b
$ (Template SpecType -> SpecType)
-> [Template SpecType] -> [SpecType]
forall a b. (a -> b) -> [a] -> [b]
map Template SpecType -> SpecType
forall t. Template t -> t
unTemplate [Template SpecType]
ts]) (([Var], [Int]) -> [(([Var], [Int]), (Var, [Int], SpecType))])
-> [([Var], [Int])] -> [[(([Var], [Int]), (Var, [Int], SpecType))]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([[Var]] -> [[Int]] -> [([Var], [Int])]
forall a b. [a] -> [b] -> [(a, b)]
zip [[Var]]
vs [[Int]]
is)
       ([[Maybe SpecType]] -> [[Maybe SpecType]]
forall a. [[a]] -> [[a]]
L.transpose ([[Maybe SpecType]] -> [[Maybe SpecType]])
-> StateT CGInfo Identity [[Maybe SpecType]]
-> StateT CGInfo Identity [[Maybe SpecType]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Var, [Var], Template SpecType, [Int])
 -> StateT CGInfo Identity [Maybe SpecType])
-> [(Var, [Var], Template SpecType, [Int])]
-> StateT CGInfo Identity [[Maybe SpecType]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Var, [Var], Template SpecType, [Int])
-> StateT CGInfo Identity [Maybe SpecType]
forall t a c tv r.
(NamedThing t, PPrint t, PPrint a) =>
(t, [a], Template (RType c tv r), [Int])
-> CG [Maybe (RType c tv r)]
checkIndex ([Var]
-> [[Var]]
-> [Template SpecType]
-> [[Int]]
-> [(Var, [Var], Template SpecType, [Int])]
forall t t1 t2 t3. [t] -> [t1] -> [t2] -> [t3] -> [(t, t1, t2, t3)]
zip4 [Var]
xs [[Var]]
vs [Template SpecType]
ts [[Int]]
is)) StateT CGInfo Identity [[Maybe SpecType]]
-> ([[Maybe SpecType]] -> StateT CGInfo Identity [[SpecType]])
-> StateT CGInfo Identity [[SpecType]]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [[Maybe SpecType]] -> StateT CGInfo Identity [[SpecType]]
checkEqTypes
       let rts :: [[SpecType]]
rts   = (HashSet TyCon
-> (([Var], [Int]), (Var, [Int], SpecType)) -> SpecType
forall a t.
Symbolic a =>
HashSet TyCon -> (([a], [Int]), (t, [Int], SpecType)) -> SpecType
recType HashSet TyCon
autoenv ((([Var], [Int]), (Var, [Int], SpecType)) -> SpecType)
-> [(([Var], [Int]), (Var, [Int], SpecType))] -> [SpecType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) ([(([Var], [Int]), (Var, [Int], SpecType))] -> [SpecType])
-> [[(([Var], [Int]), (Var, [Int], SpecType))]] -> [[SpecType]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [[(([Var], [Int]), (Var, [Int], SpecType))]]
xeets
       let xts :: [(Var, Template SpecType)]
xts   = [Var] -> [Template SpecType] -> [(Var, Template SpecType)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Var]
xs [Template SpecType]
ts
       CGEnv
γ'       <- (CGEnv -> (Var, Template SpecType) -> CG CGEnv)
-> CGEnv -> [(Var, Template SpecType)] -> CG CGEnv
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM CGEnv -> (Var, Template SpecType) -> CG CGEnv
forall a. Symbolic a => CGEnv -> (a, Template SpecType) -> CG CGEnv
extender CGEnv
γ [(Var, Template SpecType)]
xts
       let γs :: [CGEnv]
γs    = (CGEnv -> [Var] -> CGEnv) -> [CGEnv] -> [[Var]] -> [CGEnv]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith CGEnv -> [Var] -> CGEnv
makeRecInvariants [CGEnv
γ' CGEnv -> [(Var, SpecType)] -> CGEnv
`setTRec` [Var] -> [SpecType] -> [(Var, SpecType)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Var]
xs [SpecType]
rts' | [SpecType]
rts' <- [[SpecType]]
rts] ((Var -> Bool) -> [Var] -> [Var]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Var -> Bool) -> Var -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> Bool
GM.isPredVar) ([Var] -> [Var]) -> [[Var]] -> [[Var]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [[Var]]
vs)
       let xets' :: [(Var, CoreExpr, Template SpecType)]
xets' = [Var]
-> [CoreExpr]
-> [Template SpecType]
-> [(Var, CoreExpr, Template SpecType)]
forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
zip3 [Var]
xs [CoreExpr]
es [Template SpecType]
ts
       ((CGEnv, (Var, CoreExpr, Template SpecType))
 -> StateT CGInfo Identity (Template SpecType))
-> [(CGEnv, (Var, CoreExpr, Template SpecType))] -> State CGInfo ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((CGEnv
 -> (Var, CoreExpr, Template SpecType)
 -> StateT CGInfo Identity (Template SpecType))
-> (CGEnv, (Var, CoreExpr, Template SpecType))
-> StateT CGInfo Identity (Template SpecType)
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((CGEnv
  -> (Var, CoreExpr, Template SpecType)
  -> StateT CGInfo Identity (Template SpecType))
 -> (CGEnv, (Var, CoreExpr, Template SpecType))
 -> StateT CGInfo Identity (Template SpecType))
-> (CGEnv
    -> (Var, CoreExpr, Template SpecType)
    -> StateT CGInfo Identity (Template SpecType))
-> (CGEnv, (Var, CoreExpr, Template SpecType))
-> StateT CGInfo Identity (Template SpecType)
forall a b. (a -> b) -> a -> b
$ Bool
-> CGEnv
-> (Var, CoreExpr, Template SpecType)
-> StateT CGInfo Identity (Template SpecType)
consBind Bool
True) ([CGEnv]
-> [(Var, CoreExpr, Template SpecType)]
-> [(CGEnv, (Var, CoreExpr, Template SpecType))]
forall a b. [a] -> [b] -> [(a, b)]
zip [CGEnv]
γs [(Var, CoreExpr, Template SpecType)]
xets')
       CGEnv -> CG CGEnv
forall (m :: * -> *) a. Monad m => a -> m a
return CGEnv
γ'
  where
       ([Var]
xs, [CoreExpr]
es)       = [(Var, CoreExpr)] -> ([Var], [CoreExpr])
forall a b. [(a, b)] -> ([a], [b])
unzip [(Var, CoreExpr)]
xes
       dxs :: [Doc]
dxs            = Var -> Doc
forall a. PPrint a => a -> Doc
F.pprint (Var -> Doc) -> [Var] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Var]
xs
       collectArgs :: Template (RType c tv r) -> CoreExpr -> [Var]
collectArgs    = Int -> CoreExpr -> [Var]
GM.collectArguments (Int -> CoreExpr -> [Var])
-> (Template (RType c tv r) -> Int)
-> Template (RType c tv r)
-> CoreExpr
-> [Var]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Symbol] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([Symbol] -> Int)
-> (Template (RType c tv r) -> [Symbol])
-> Template (RType c tv r)
-> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTypeRep c tv r -> [Symbol]
forall c tv r. RTypeRep c tv r -> [Symbol]
ty_binds (RTypeRep c tv r -> [Symbol])
-> (Template (RType c tv r) -> RTypeRep c tv r)
-> Template (RType c tv r)
-> [Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RType c tv r -> RTypeRep c tv r
forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep (RType c tv r -> RTypeRep c tv r)
-> (Template (RType c tv r) -> RType c tv r)
-> Template (RType c tv r)
-> RTypeRep c tv r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RType c tv r -> RType c tv r
forall c tv r. RType c tv r -> RType c tv r
unOCons (RType c tv r -> RType c tv r)
-> (Template (RType c tv r) -> RType c tv r)
-> Template (RType c tv r)
-> RType c tv r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Template (RType c tv r) -> RType c tv r
forall t. Template t -> t
unTemplate
       checkEqTypes :: [[Maybe SpecType]] -> CG [[SpecType]]
       checkEqTypes :: [[Maybe SpecType]] -> StateT CGInfo Identity [[SpecType]]
checkEqTypes [[Maybe SpecType]]
x = ([SpecType] -> StateT CGInfo Identity [SpecType])
-> [[SpecType]] -> StateT CGInfo Identity [[SpecType]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (TError SpecType
-> (SpecType -> RType RTyCon RTyVar ())
-> [SpecType]
-> StateT CGInfo Identity [SpecType]
forall b a.
Eq b =>
TError SpecType -> (a -> b) -> [a] -> StateT CGInfo Identity [a]
checkAll TError SpecType
forall t. TError t
err1 SpecType -> RType RTyCon RTyVar ()
forall c tv r. RType c tv r -> RType c tv ()
toRSort) ([Maybe SpecType] -> [SpecType]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe SpecType] -> [SpecType])
-> [[Maybe SpecType]] -> [[SpecType]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [[Maybe SpecType]]
x)
       checkSameLens :: [t a] -> StateT CGInfo Identity [t a]
checkSameLens  = TError SpecType
-> (t a -> Int) -> [t a] -> StateT CGInfo Identity [t a]
forall b a.
Eq b =>
TError SpecType -> (a -> b) -> [a] -> StateT CGInfo Identity [a]
checkAll TError SpecType
forall t. TError t
err2 t a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length
       err1 :: TError t
err1           = SrcSpan -> [Doc] -> Doc -> TError t
forall t. SrcSpan -> [Doc] -> Doc -> TError t
ErrTermin SrcSpan
loc [Doc]
dxs (Doc -> TError t) -> Doc -> TError t
forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
"The decreasing parameters should be of same type"
       err2 :: TError t
err2           = SrcSpan -> [Doc] -> Doc -> TError t
forall t. SrcSpan -> [Doc] -> Doc -> TError t
ErrTermin SrcSpan
loc [Doc]
dxs (Doc -> TError t) -> Doc -> TError t
forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
"All Recursive functions should have the same number of decreasing parameters"
       loc :: SrcSpan
loc            = Var -> SrcSpan
forall a. NamedThing a => a -> SrcSpan
getSrcSpan ([Var] -> Var
forall a. [a] -> a
head [Var]
xs)

       checkAll :: TError SpecType -> (a -> b) -> [a] -> StateT CGInfo Identity [a]
checkAll TError SpecType
_   a -> b
_ []            = [a] -> StateT CGInfo Identity [a]
forall (m :: * -> *) a. Monad m => a -> m a
return []
       checkAll TError SpecType
err a -> b
f (a
x:[a]
xs)
         | (b -> Bool) -> [b] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (b -> b -> Bool
forall a. Eq a => a -> a -> Bool
==(a -> b
f a
x)) (a -> b
f (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a]
xs) = [a] -> StateT CGInfo Identity [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (a
xa -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
xs)
         | Bool
otherwise                = TError SpecType -> State CGInfo ()
addWarning TError SpecType
err State CGInfo ()
-> StateT CGInfo Identity [a] -> StateT CGInfo Identity [a]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [a] -> StateT CGInfo Identity [a]
forall (m :: * -> *) a. Monad m => a -> m a
return []

consCBWithExprs :: CGEnv -> [(Var, CoreExpr)] -> CG CGEnv
consCBWithExprs :: CGEnv -> [(Var, CoreExpr)] -> CG CGEnv
consCBWithExprs CGEnv
γ [(Var, CoreExpr)]
xes
  = do [(Var, CoreExpr, Template SpecType)]
xets     <- [(Var, CoreExpr)]
-> ((Var, CoreExpr)
    -> StateT CGInfo Identity (Var, CoreExpr, Template SpecType))
-> StateT CGInfo Identity [(Var, CoreExpr, Template SpecType)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Var, CoreExpr)]
xes (((Var, CoreExpr)
  -> StateT CGInfo Identity (Var, CoreExpr, Template SpecType))
 -> StateT CGInfo Identity [(Var, CoreExpr, Template SpecType)])
-> ((Var, CoreExpr)
    -> StateT CGInfo Identity (Var, CoreExpr, Template SpecType))
-> StateT CGInfo Identity [(Var, CoreExpr, Template SpecType)]
forall a b. (a -> b) -> a -> b
$ \(Var
x, CoreExpr
e) -> (Template SpecType -> (Var, CoreExpr, Template SpecType))
-> StateT CGInfo Identity (Template SpecType)
-> StateT CGInfo Identity (Var, CoreExpr, Template SpecType)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (Var
x, CoreExpr
e,) (CGEnv
-> (Var, Maybe CoreExpr)
-> StateT CGInfo Identity (Template SpecType)
varTemplate CGEnv
γ (Var
x, CoreExpr -> Maybe CoreExpr
forall a. a -> Maybe a
Just CoreExpr
e))
       HashMap Var [Located Expr]
texprs    <- CGInfo -> HashMap Var [Located Expr]
termExprs (CGInfo -> HashMap Var [Located Expr])
-> StateT CGInfo Identity CGInfo
-> StateT CGInfo Identity (HashMap Var [Located Expr])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT CGInfo Identity CGInfo
forall s (m :: * -> *). MonadState s m => m s
get
       let xtes :: [(Var, [Located Expr])]
xtes   = [Maybe (Var, [Located Expr])] -> [(Var, [Located Expr])]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe (Var, [Located Expr])] -> [(Var, [Located Expr])])
-> [Maybe (Var, [Located Expr])] -> [(Var, [Located Expr])]
forall a b. (a -> b) -> a -> b
$ (Var -> HashMap Var [Located Expr] -> Maybe (Var, [Located Expr])
forall a b. (Eq a, Hashable a) => a -> HashMap a b -> Maybe (a, b)
`lookup` HashMap Var [Located Expr]
texprs) (Var -> Maybe (Var, [Located Expr]))
-> [Var] -> [Maybe (Var, [Located Expr])]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Var]
xs
       let ts :: [SpecType]
ts    = String -> Template SpecType -> SpecType
forall t. String -> Template t -> t
safeFromAsserted String
forall p. IsString p => p
err (Template SpecType -> SpecType)
-> ((Var, CoreExpr, Template SpecType) -> Template SpecType)
-> (Var, CoreExpr, Template SpecType)
-> SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Var, CoreExpr, Template SpecType) -> Template SpecType
forall a b c. (a, b, c) -> c
thd3 ((Var, CoreExpr, Template SpecType) -> SpecType)
-> [(Var, CoreExpr, Template SpecType)] -> [SpecType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Var, CoreExpr, Template SpecType)]
xets
       [SpecType]
ts'      <- (SpecType -> CG SpecType)
-> [SpecType] -> StateT CGInfo Identity [SpecType]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM SpecType -> CG SpecType
forall (m :: * -> *). FreshM m => SpecType -> m SpecType
refreshArgs [SpecType]
ts
       let xts :: [(Var, Template SpecType)]
xts   = [Var] -> [Template SpecType] -> [(Var, Template SpecType)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Var]
xs (SpecType -> Template SpecType
forall a. a -> Template a
Asserted (SpecType -> Template SpecType)
-> [SpecType] -> [Template SpecType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SpecType]
ts')
       CGEnv
γ'       <- (CGEnv -> (Var, Template SpecType) -> CG CGEnv)
-> CGEnv -> [(Var, Template SpecType)] -> CG CGEnv
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM CGEnv -> (Var, Template SpecType) -> CG CGEnv
forall a. Symbolic a => CGEnv -> (a, Template SpecType) -> CG CGEnv
extender CGEnv
γ [(Var, Template SpecType)]
xts
       let γs :: [CGEnv]
γs    = CGEnv
-> [(Var, [Located Expr])]
-> [(Var, CoreExpr)]
-> [SpecType]
-> [SpecType]
-> [CGEnv]
makeTermEnvs CGEnv
γ' [(Var, [Located Expr])]
xtes [(Var, CoreExpr)]
xes [SpecType]
ts [SpecType]
ts'
       let xets' :: [(Var, CoreExpr, Template SpecType)]
xets' = [Var]
-> [CoreExpr]
-> [Template SpecType]
-> [(Var, CoreExpr, Template SpecType)]
forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
zip3 [Var]
xs [CoreExpr]
es (SpecType -> Template SpecType
forall a. a -> Template a
Asserted (SpecType -> Template SpecType)
-> [SpecType] -> [Template SpecType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SpecType]
ts')
       ((CGEnv, (Var, CoreExpr, Template SpecType))
 -> StateT CGInfo Identity (Template SpecType))
-> [(CGEnv, (Var, CoreExpr, Template SpecType))] -> State CGInfo ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((CGEnv
 -> (Var, CoreExpr, Template SpecType)
 -> StateT CGInfo Identity (Template SpecType))
-> (CGEnv, (Var, CoreExpr, Template SpecType))
-> StateT CGInfo Identity (Template SpecType)
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((CGEnv
  -> (Var, CoreExpr, Template SpecType)
  -> StateT CGInfo Identity (Template SpecType))
 -> (CGEnv, (Var, CoreExpr, Template SpecType))
 -> StateT CGInfo Identity (Template SpecType))
-> (CGEnv
    -> (Var, CoreExpr, Template SpecType)
    -> StateT CGInfo Identity (Template SpecType))
-> (CGEnv, (Var, CoreExpr, Template SpecType))
-> StateT CGInfo Identity (Template SpecType)
forall a b. (a -> b) -> a -> b
$ Bool
-> CGEnv
-> (Var, CoreExpr, Template SpecType)
-> StateT CGInfo Identity (Template SpecType)
consBind Bool
True) ([CGEnv]
-> [(Var, CoreExpr, Template SpecType)]
-> [(CGEnv, (Var, CoreExpr, Template SpecType))]
forall a b. [a] -> [b] -> [(a, b)]
zip [CGEnv]
γs [(Var, CoreExpr, Template SpecType)]
xets')
       CGEnv -> CG CGEnv
forall (m :: * -> *) a. Monad m => a -> m a
return CGEnv
γ'
  where ([Var]
xs, [CoreExpr]
es) = [(Var, CoreExpr)] -> ([Var], [CoreExpr])
forall a b. [(a, b)] -> ([a], [b])
unzip [(Var, CoreExpr)]
xes
        lookup :: a -> HashMap a b -> Maybe (a, b)
lookup a
k HashMap a b
m | Just b
x <- a -> HashMap a b -> Maybe b
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup a
k HashMap a b
m = (a, b) -> Maybe (a, b)
forall a. a -> Maybe a
Just (a
k, b
x)
                   | Bool
otherwise              = Maybe (a, b)
forall a. Maybe a
Nothing
        err :: p
err      = p
"Constant: consCBWithExprs"

makeTermEnvs :: CGEnv -> [(Var, [F.Located F.Expr])] -> [(Var, CoreExpr)]
             -> [SpecType] -> [SpecType]
             -> [CGEnv]
makeTermEnvs :: CGEnv
-> [(Var, [Located Expr])]
-> [(Var, CoreExpr)]
-> [SpecType]
-> [SpecType]
-> [CGEnv]
makeTermEnvs CGEnv
γ [(Var, [Located Expr])]
xtes [(Var, CoreExpr)]
xes [SpecType]
ts [SpecType]
ts' = CGEnv -> [(Var, SpecType)] -> CGEnv
setTRec CGEnv
γ ([(Var, SpecType)] -> CGEnv)
-> ([SpecType] -> [(Var, SpecType)]) -> [SpecType] -> CGEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Var] -> [SpecType] -> [(Var, SpecType)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Var]
xs ([SpecType] -> CGEnv) -> [[SpecType]] -> [CGEnv]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [[SpecType]]
rts
  where
    vs :: [[Var]]
vs   = (SpecType -> CoreExpr -> [Var])
-> [SpecType] -> [CoreExpr] -> [[Var]]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith SpecType -> CoreExpr -> [Var]
forall c tv r. RType c tv r -> CoreExpr -> [Var]
collectArgs [SpecType]
ts [CoreExpr]
es
    ys :: [[Symbol]]
ys   = (([Symbol], [SpecType], [RReft], SpecType) -> [Symbol]
forall t t1 t2 t3. (t, t1, t2, t3) -> t
fst4 (([Symbol], [SpecType], [RReft], SpecType) -> [Symbol])
-> (SpecType -> ([Symbol], [SpecType], [RReft], SpecType))
-> SpecType
-> [Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SpecType -> ([Symbol], [SpecType], [RReft], SpecType)
forall t t1 a.
RType t t1 a -> ([Symbol], [RType t t1 a], [a], RType t t1 a)
bkArrowDeep) (SpecType -> [Symbol]) -> [SpecType] -> [[Symbol]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SpecType]
ts
    ys' :: [[Symbol]]
ys'  = (([Symbol], [SpecType], [RReft], SpecType) -> [Symbol]
forall t t1 t2 t3. (t, t1, t2, t3) -> t
fst4 (([Symbol], [SpecType], [RReft], SpecType) -> [Symbol])
-> (SpecType -> ([Symbol], [SpecType], [RReft], SpecType))
-> SpecType
-> [Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SpecType -> ([Symbol], [SpecType], [RReft], SpecType)
forall t t1 a.
RType t t1 a -> ([Symbol], [RType t t1 a], [a], RType t t1 a)
bkArrowDeep) (SpecType -> [Symbol]) -> [SpecType] -> [[Symbol]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SpecType]
ts'
    sus' :: [Subst]
sus' = ([Symbol] -> [Symbol] -> Subst)
-> [[Symbol]] -> [[Symbol]] -> [Subst]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith [Symbol] -> [Symbol] -> Subst
mkSub [[Symbol]]
ys [[Symbol]]
ys'
    sus :: [Subst]
sus  = ([Symbol] -> [Symbol] -> Subst)
-> [[Symbol]] -> [[Symbol]] -> [Subst]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith [Symbol] -> [Symbol] -> Subst
mkSub [[Symbol]]
ys ((Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (Var -> Symbol) -> [Var] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) ([Var] -> [Symbol]) -> [[Var]] -> [[Symbol]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [[Var]]
vs)
    ess :: [[Located Expr]]
ess  = (\Var
x -> (String -> Maybe [Located Expr] -> [Located Expr]
forall t. String -> Maybe t -> t
safeFromJust (Var -> String
forall a. Outputable a => a -> String
err Var
x) (Maybe [Located Expr] -> [Located Expr])
-> Maybe [Located Expr] -> [Located Expr]
forall a b. (a -> b) -> a -> b
$ (Var
x Var -> [(Var, [Located Expr])] -> Maybe [Located Expr]
forall a b. Eq a => a -> [(a, b)] -> Maybe b
`L.lookup` [(Var, [Located Expr])]
xtes))) (Var -> [Located Expr]) -> [Var] -> [[Located Expr]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Var]
xs
    tes :: [[Located Expr]]
tes  = (Subst -> [Located Expr] -> [Located Expr])
-> [Subst] -> [[Located Expr]] -> [[Located Expr]]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Subst
su [Located Expr]
es -> Subst -> Located Expr -> Located Expr
forall a. Subable a => Subst -> a -> a
F.subst Subst
su (Located Expr -> Located Expr) -> [Located Expr] -> [Located Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Located Expr]
es)  [Subst]
sus [[Located Expr]]
ess
    tes' :: [[Located Expr]]
tes' = (Subst -> [Located Expr] -> [Located Expr])
-> [Subst] -> [[Located Expr]] -> [[Located Expr]]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Subst
su [Located Expr]
es -> Subst -> Located Expr -> Located Expr
forall a. Subable a => Subst -> a -> a
F.subst Subst
su (Located Expr -> Located Expr) -> [Located Expr] -> [Located Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Located Expr]
es)  [Subst]
sus' [[Located Expr]]
ess
    rss :: [[RReft]]
rss  = ([Located Expr] -> [Located Expr] -> RReft)
-> [[Located Expr]] -> [[Located Expr]] -> [RReft]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith [Located Expr] -> [Located Expr] -> RReft
makeLexRefa [[Located Expr]]
tes' ([[Located Expr]] -> [RReft]) -> [[[Located Expr]]] -> [[RReft]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Located Expr] -> [[Located Expr]]
forall a. a -> [a]
repeat ([Located Expr] -> [[Located Expr]])
-> [[Located Expr]] -> [[[Located Expr]]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [[Located Expr]]
tes)
    rts :: [[SpecType]]
rts  = (SpecType -> RReft -> SpecType)
-> [SpecType] -> [RReft] -> [SpecType]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (Oblig -> SpecType -> RReft -> SpecType
addObligation Oblig
OTerm) [SpecType]
ts' ([RReft] -> [SpecType]) -> [[RReft]] -> [[SpecType]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [[RReft]]
rss
    ([Var]
xs, [CoreExpr]
es)     = [(Var, CoreExpr)] -> ([Var], [CoreExpr])
forall a b. [(a, b)] -> ([a], [b])
unzip [(Var, CoreExpr)]
xes
    mkSub :: [Symbol] -> [Symbol] -> Subst
mkSub [Symbol]
ys [Symbol]
ys' = [(Symbol, Expr)] -> Subst
F.mkSubst [(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]
ys [Symbol]
ys']
    collectArgs :: RType c tv r -> CoreExpr -> [Var]
collectArgs  = Int -> CoreExpr -> [Var]
GM.collectArguments (Int -> CoreExpr -> [Var])
-> (RType c tv r -> Int) -> RType c tv r -> CoreExpr -> [Var]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Symbol] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([Symbol] -> Int)
-> (RType c tv r -> [Symbol]) -> RType c tv r -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTypeRep c tv r -> [Symbol]
forall c tv r. RTypeRep c tv r -> [Symbol]
ty_binds (RTypeRep c tv r -> [Symbol])
-> (RType c tv r -> RTypeRep c tv r) -> RType c tv r -> [Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RType c tv r -> RTypeRep c tv r
forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep
    err :: a -> String
err a
x        = String
"Constant: makeTermEnvs: no terminating expression for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Outputable a => a -> String
GM.showPpr a
x

addObligation :: Oblig -> SpecType -> RReft -> SpecType
addObligation :: Oblig -> SpecType -> RReft -> SpecType
addObligation Oblig
o SpecType
t RReft
r  = [(RTVar RTyVar (RType RTyCon RTyVar ()), RReft)]
-> [PVar (RType RTyCon RTyVar ())]
-> [(Symbol, SpecType, RReft)]
-> [(Symbol, SpecType, RReft)]
-> SpecType
-> SpecType
forall tv c r.
[(RTVar tv (RType c tv ()), r)]
-> [PVar (RType c tv ())]
-> [(Symbol, RType c tv r, r)]
-> [(Symbol, RType c tv r, r)]
-> RType c tv r
-> RType c tv r
mkArrow [(RTVar RTyVar (RType RTyCon RTyVar ()), RReft)]
αs [PVar (RType RTyCon RTyVar ())]
πs [(Symbol, SpecType, RReft)]
yts [(Symbol, SpecType, RReft)]
xts (SpecType -> SpecType) -> SpecType -> SpecType
forall a b. (a -> b) -> a -> b
$ [(Symbol, SpecType)] -> RReft -> Oblig -> SpecType -> SpecType
forall c tv r.
[(Symbol, RType c tv r)]
-> r -> Oblig -> RType c tv r -> RType c tv r
RRTy [] RReft
r Oblig
o SpecType
t2
  where
    ([(RTVar RTyVar (RType RTyCon RTyVar ()), RReft)]
αs, [PVar (RType RTyCon RTyVar ())]
πs, SpecType
t1) = 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
t
    (([Symbol]
xs',[SpecType]
ts',[RReft]
rs'),([Symbol]
xs, [SpecType]
ts, [RReft]
rs), SpecType
t2) = SpecType
-> (([Symbol], [SpecType], [RReft]),
    ([Symbol], [SpecType], [RReft]), SpecType)
forall t t1 a.
RType t t1 a
-> (([Symbol], [RType t t1 a], [a]),
    ([Symbol], [RType t t1 a], [a]), RType t t1 a)
bkArrow SpecType
t1
    xts :: [(Symbol, SpecType, RReft)]
xts              = [Symbol] -> [SpecType] -> [RReft] -> [(Symbol, SpecType, RReft)]
forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
zip3 [Symbol]
xs [SpecType]
ts [RReft]
rs
    yts :: [(Symbol, SpecType, RReft)]
yts              = [Symbol] -> [SpecType] -> [RReft] -> [(Symbol, SpecType, RReft)]
forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
zip3 [Symbol]
xs' [SpecType]
ts' [RReft]
rs'

--------------------------------------------------------------------------------
consCB :: Bool -> Bool -> CGEnv -> CoreBind -> CG CGEnv
--------------------------------------------------------------------------------
-- do termination checking
consCB :: Bool -> Bool -> CGEnv -> CoreBind -> CG CGEnv
consCB Bool
True Bool
_ CGEnv
γ (Rec [(Var, CoreExpr)]
xes)
  = do HashMap Var [Located Expr]
texprs <- CGInfo -> HashMap Var [Located Expr]
termExprs (CGInfo -> HashMap Var [Located Expr])
-> StateT CGInfo Identity CGInfo
-> StateT CGInfo Identity (HashMap Var [Located Expr])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT CGInfo Identity CGInfo
forall s (m :: * -> *). MonadState s m => m s
get
       (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 :: Int
recCount = CGInfo -> Int
recCount CGInfo
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [(Var, CoreExpr)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Var, CoreExpr)]
xes }
       let xxes :: [(Var, [Located Expr])]
xxes = [Maybe (Var, [Located Expr])] -> [(Var, [Located Expr])]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe (Var, [Located Expr])] -> [(Var, [Located Expr])])
-> [Maybe (Var, [Located Expr])] -> [(Var, [Located Expr])]
forall a b. (a -> b) -> a -> b
$ (Var -> HashMap Var [Located Expr] -> Maybe (Var, [Located Expr])
forall a b. (Eq a, Hashable a) => a -> HashMap a b -> Maybe (a, b)
`lookup` HashMap Var [Located Expr]
texprs) (Var -> Maybe (Var, [Located Expr]))
-> [Var] -> [Maybe (Var, [Located Expr])]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Var]
xs
       if [(Var, [Located Expr])] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Var, [Located Expr])]
xxes
         then CGEnv -> [(Var, CoreExpr)] -> CG CGEnv
consCBSizedTys CGEnv
γ [(Var, CoreExpr)]
xes
         else [(Var, [Located Expr])] -> CGEnv -> CGEnv
forall (t :: * -> *) a p. Foldable t => t a -> p -> p
check [(Var, [Located Expr])]
xxes (CGEnv -> CGEnv) -> CG CGEnv -> CG CGEnv
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CGEnv -> [(Var, CoreExpr)] -> CG CGEnv
consCBWithExprs CGEnv
γ [(Var, CoreExpr)]
xes
    where
      xs :: [Var]
xs = ([Var], [CoreExpr]) -> [Var]
forall a b. (a, b) -> a
fst ([(Var, CoreExpr)] -> ([Var], [CoreExpr])
forall a b. [(a, b)] -> ([a], [b])
unzip [(Var, CoreExpr)]
xes)
      check :: t a -> p -> p
check t a
ys p
r | t a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length t a
ys Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Var] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Var]
xs = p
r
                 | Bool
otherwise              = Maybe SrcSpan -> String -> p
forall a. Maybe SrcSpan -> String -> a
panic (SrcSpan -> Maybe SrcSpan
forall a. a -> Maybe a
Just SrcSpan
loc) (String -> p) -> String -> p
forall a b. (a -> b) -> a -> b
$ String
forall p. IsString p => p
msg
      msg :: p
msg        = p
"Termination expressions must be provided for all mutually recursive binders"
      loc :: SrcSpan
loc        = Var -> SrcSpan
forall a. NamedThing a => a -> SrcSpan
getSrcSpan ([Var] -> Var
forall a. [a] -> a
head [Var]
xs)
      lookup :: k -> HashMap k t -> Maybe (k, t)
lookup k
k HashMap k t
m = (k
k,) (t -> (k, t)) -> Maybe t -> Maybe (k, t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> k -> HashMap k t -> Maybe t
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup k
k HashMap k t
m

-- don't do termination checking, but some strata checks?
consCB Bool
_ Bool
False CGEnv
γ (Rec [(Var, CoreExpr)]
xes)
  = do [(Var, CoreExpr, Template SpecType)]
xets     <- [(Var, CoreExpr)]
-> ((Var, CoreExpr)
    -> StateT CGInfo Identity (Var, CoreExpr, Template SpecType))
-> StateT CGInfo Identity [(Var, CoreExpr, Template SpecType)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Var, CoreExpr)]
xes (((Var, CoreExpr)
  -> StateT CGInfo Identity (Var, CoreExpr, Template SpecType))
 -> StateT CGInfo Identity [(Var, CoreExpr, Template SpecType)])
-> ((Var, CoreExpr)
    -> StateT CGInfo Identity (Var, CoreExpr, Template SpecType))
-> StateT CGInfo Identity [(Var, CoreExpr, Template SpecType)]
forall a b. (a -> b) -> a -> b
$ \(Var
x, CoreExpr
e) -> (Var
x, CoreExpr
e,) (Template SpecType -> (Var, CoreExpr, Template SpecType))
-> StateT CGInfo Identity (Template SpecType)
-> StateT CGInfo Identity (Var, CoreExpr, Template SpecType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CGEnv
-> (Var, Maybe CoreExpr)
-> StateT CGInfo Identity (Template SpecType)
varTemplate CGEnv
γ (Var
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 :: Int
recCount = CGInfo -> Int
recCount CGInfo
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [(Var, CoreExpr)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Var, CoreExpr)]
xes }
       let xts :: [(Var, Template SpecType)]
xts    = [(Var
x, Template SpecType
to) | (Var
x, CoreExpr
_, Template SpecType
to) <- [(Var, CoreExpr, Template SpecType)]
xets]
       CGEnv
γ'        <- (CGEnv -> (Var, Template SpecType) -> CG CGEnv)
-> CGEnv -> [(Var, Template SpecType)] -> CG CGEnv
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM CGEnv -> (Var, Template SpecType) -> CG CGEnv
forall a. Symbolic a => CGEnv -> (a, Template SpecType) -> CG CGEnv
extender (CGEnv
γ CGEnv -> [Var] -> CGEnv
`setRecs` ((Var, Template SpecType) -> Var
forall a b. (a, b) -> a
fst ((Var, Template SpecType) -> Var)
-> [(Var, Template SpecType)] -> [Var]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Var, Template SpecType)]
xts)) [(Var, Template SpecType)]
xts
       ((Var, CoreExpr, Template SpecType)
 -> StateT CGInfo Identity (Template SpecType))
-> [(Var, CoreExpr, Template SpecType)] -> State CGInfo ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Bool
-> CGEnv
-> (Var, CoreExpr, Template SpecType)
-> StateT CGInfo Identity (Template SpecType)
consBind Bool
True CGEnv
γ') [(Var, CoreExpr, Template SpecType)]
xets
       CGEnv -> CG CGEnv
forall (m :: * -> *) a. Monad m => a -> m a
return CGEnv
γ'

-- don't do termination checking, and don't do any strata checks either?
consCB Bool
_ Bool
_ CGEnv
γ (Rec [(Var, CoreExpr)]
xes)
  = do [(Var, CoreExpr, Template SpecType)]
xets   <- [(Var, CoreExpr)]
-> ((Var, CoreExpr)
    -> StateT CGInfo Identity (Var, CoreExpr, Template SpecType))
-> StateT CGInfo Identity [(Var, CoreExpr, Template SpecType)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Var, CoreExpr)]
xes (((Var, CoreExpr)
  -> StateT CGInfo Identity (Var, CoreExpr, Template SpecType))
 -> StateT CGInfo Identity [(Var, CoreExpr, Template SpecType)])
-> ((Var, CoreExpr)
    -> StateT CGInfo Identity (Var, CoreExpr, Template SpecType))
-> StateT CGInfo Identity [(Var, CoreExpr, Template SpecType)]
forall a b. (a -> b) -> a -> b
$ \(Var
x, CoreExpr
e) -> (Template SpecType -> (Var, CoreExpr, Template SpecType))
-> StateT CGInfo Identity (Template SpecType)
-> StateT CGInfo Identity (Var, CoreExpr, Template SpecType)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (Var
x, CoreExpr
e,) (CGEnv
-> (Var, Maybe CoreExpr)
-> StateT CGInfo Identity (Template SpecType)
varTemplate CGEnv
γ (Var
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 :: Int
recCount = CGInfo -> Int
recCount CGInfo
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [(Var, CoreExpr)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Var, CoreExpr)]
xes }
       let xts :: [(Var, Template SpecType)]
xts = [(Var
x, Template SpecType
to) | (Var
x, CoreExpr
_, Template SpecType
to) <- [(Var, CoreExpr, Template SpecType)]
xets]
       CGEnv
γ'     <- (CGEnv -> (Var, Template SpecType) -> CG CGEnv)
-> CGEnv -> [(Var, Template SpecType)] -> CG CGEnv
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM CGEnv -> (Var, Template SpecType) -> CG CGEnv
forall a. Symbolic a => CGEnv -> (a, Template SpecType) -> CG CGEnv
extender (CGEnv
γ CGEnv -> [Var] -> CGEnv
`setRecs` ((Var, Template SpecType) -> Var
forall a b. (a, b) -> a
fst ((Var, Template SpecType) -> Var)
-> [(Var, Template SpecType)] -> [Var]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Var, Template SpecType)]
xts)) [(Var, Template SpecType)]
xts
       ((Var, CoreExpr, Template SpecType)
 -> StateT CGInfo Identity (Template SpecType))
-> [(Var, CoreExpr, Template SpecType)] -> State CGInfo ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Bool
-> CGEnv
-> (Var, CoreExpr, Template SpecType)
-> StateT CGInfo Identity (Template SpecType)
consBind Bool
True CGEnv
γ') [(Var, CoreExpr, Template SpecType)]
xets
       CGEnv -> CG CGEnv
forall (m :: * -> *) a. Monad m => a -> m a
return CGEnv
γ'

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


consCB Bool
_ Bool
_ CGEnv
γ (NonRec Var
x CoreExpr
_ ) | Var -> Bool
isHoleVar Var
x Bool -> Bool -> Bool
&& Config -> Bool
typedHoles (CGEnv -> Config
forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)
  = CGEnv -> CG CGEnv
forall (m :: * -> *) a. Monad m => a -> m a
return CGEnv
γ 

consCB Bool
_ Bool
_ CGEnv
γ (NonRec Var
x CoreExpr
def)
  | Just (Var
w, [Type]
τ) <- CoreExpr -> Maybe (Var, [Type])
grepDictionary CoreExpr
def
  , Just HashMap Symbol (RISig SpecType)
d      <- DEnv Var SpecType -> Var -> Maybe (HashMap Symbol (RISig SpecType))
forall k t.
(Eq k, Hashable k) =>
DEnv k t -> k -> Maybe (HashMap Symbol (RISig t))
dlookup (CGEnv -> DEnv Var SpecType
denv CGEnv
γ) Var
w
  = do [SpecType]
t        <- (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)
mapM Type -> CG SpecType
trueTy [Type]
τ
       (WfC -> State CGInfo ()) -> [WfC] -> StateT CGInfo Identity [()]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
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]
t)
       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 (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 ())), Eq tv) =>
[RType c tv r] -> RType c tv r -> RType c tv r
f [SpecType]
t)) HashMap Symbol (RISig SpecType)
d
       let  γ' :: CGEnv
γ'   = CGEnv
γ { denv :: DEnv Var SpecType
denv = DEnv Var SpecType
-> Var -> HashMap Symbol (RISig SpecType) -> DEnv Var SpecType
forall x ty.
(Eq x, Hashable x) =>
DEnv x ty -> x -> HashMap Symbol (RISig ty) -> DEnv x ty
dinsert (CGEnv -> DEnv Var SpecType
denv CGEnv
γ) Var
x HashMap Symbol (RISig SpecType)
xts }
       SpecType
t        <- Type -> CG SpecType
trueTy (Var -> Type
varType Var
x)
       CGEnv -> (Var, Template SpecType) -> CG CGEnv
forall a. Symbolic a => CGEnv -> (a, Template SpecType) -> CG CGEnv
extender CGEnv
γ' (Var
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
subsTyVar_meet' (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
subsTyVar_meet' (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 -> String -> RType c tv r
forall a. Maybe SrcSpan -> String -> a
impossible Maybe SrcSpan
forall a. Maybe a
Nothing String
"consCB on Dictionary: this should not happen"

consCB Bool
_ Bool
_ CGEnv
γ (NonRec Var
x CoreExpr
e)
  = do Template SpecType
to  <- CGEnv
-> (Var, Maybe CoreExpr)
-> StateT CGInfo Identity (Template SpecType)
varTemplate CGEnv
γ (Var
x, Maybe CoreExpr
forall a. Maybe a
Nothing)
       Template SpecType
to' <- Bool
-> CGEnv
-> (Var, CoreExpr, Template SpecType)
-> StateT CGInfo Identity (Template SpecType)
consBind Bool
False CGEnv
γ (Var
x, CoreExpr
e, Template SpecType
to) StateT CGInfo Identity (Template SpecType)
-> (Template SpecType
    -> StateT CGInfo Identity (Template SpecType))
-> StateT CGInfo Identity (Template SpecType)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (CGEnv
-> Template SpecType -> StateT CGInfo Identity (Template SpecType)
addPostTemplate CGEnv
γ)
       CGEnv -> (Var, Template SpecType) -> CG CGEnv
forall a. Symbolic a => CGEnv -> (a, Template SpecType) -> CG CGEnv
extender CGEnv
γ (Var
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 (Var, [Type])
grepDictionary = [Type] -> CoreExpr -> Maybe (Var, [Type])
forall b. [Type] -> Expr b -> Maybe (Var, [Type])
go [] 
  where 
    go :: [Type] -> Expr b -> Maybe (Var, [Type])
go [Type]
ts (App (Var Var
w) (Type Type
t)) = (Var, [Type]) -> Maybe (Var, [Type])
forall a. a -> Maybe a
Just (Var
w, [Type] -> [Type]
forall a. [a] -> [a]
reverse (Type
tType -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:[Type]
ts))
    go [Type]
ts (App Expr b
e (Type Type
t))       = [Type] -> Expr b -> Maybe (Var, [Type])
go (Type
tType -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:[Type]
ts) Expr b
e
    go [Type]
ts (App Expr b
e (Var Var
_))        = [Type] -> Expr b -> Maybe (Var, [Type])
go [Type]
ts Expr b
e
    go [Type]
_ Expr b
_                       = Maybe (Var, [Type])
forall a. Maybe a
Nothing

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

consBind Bool
isRec CGEnv
γ (Var
x, CoreExpr
e, Asserted SpecType
spect)
  = do let γ' :: CGEnv
γ'       = CGEnv
γ CGEnv -> Var -> CGEnv
`setBind` Var
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

       -- take implcits out of the function's SpecType and into the env
       let tyr :: RTypeRep RTyCon RTyVar RReft
tyr = SpecType -> RTypeRep RTyCon RTyVar RReft
forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep SpecType
spect
       let spect' :: SpecType
spect' = RTypeRep RTyCon RTyVar RReft -> SpecType
forall c tv r. RTypeRep c tv r -> RType c tv r
fromRTypeRep (RTypeRep RTyCon RTyVar RReft
tyr { ty_ebinds :: [Symbol]
ty_ebinds = [], ty_eargs :: [SpecType]
ty_eargs = [], ty_erefts :: [RReft]
ty_erefts = [] })
       CGEnv
γπ <- (CGEnv -> (String, Symbol, SpecType) -> CG CGEnv)
-> CGEnv -> [(String, Symbol, SpecType)] -> CG CGEnv
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM CGEnv -> (String, Symbol, SpecType) -> CG CGEnv
(+=) CGEnv
γπ ([(String, Symbol, SpecType)] -> CG CGEnv)
-> [(String, Symbol, SpecType)] -> CG CGEnv
forall a b. (a -> b) -> a -> b
$ (\(Symbol
y,SpecType
t)->(String
"implicitError",Symbol
y,SpecType
t)) ((Symbol, SpecType) -> (String, Symbol, SpecType))
-> [(Symbol, SpecType)] -> [(String, Symbol, SpecType)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol] -> [SpecType] -> [(Symbol, SpecType)]
forall a b. [a] -> [b] -> [(a, b)]
zip (RTypeRep RTyCon RTyVar RReft -> [Symbol]
forall c tv r. RTypeRep c tv r -> [Symbol]
ty_ebinds RTypeRep RTyCon RTyVar RReft
tyr) (RTypeRep RTyCon RTyVar RReft -> [SpecType]
forall c tv r. RTypeRep c tv r -> [RType c tv r]
ty_eargs RTypeRep RTyCon RTyVar RReft
tyr)

       CGEnv -> CoreExpr -> SpecType -> State CGInfo ()
cconsE CGEnv
γπ CoreExpr
e (Var -> SpecType -> SpecType
weakenResult Var
x SpecType
spect')
       Bool -> State CGInfo () -> State CGInfo ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
x Symbol -> HEnv -> Bool
`elemHEnv` CGEnv -> HEnv
holes CGEnv
γ) (State CGInfo () -> State CGInfo ())
-> State CGInfo () -> State CGInfo ()
forall a b. (a -> b) -> a -> b
$
         -- have to add the wf constraint here for HOLEs so we have the proper env
         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 (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap RReft -> RReft
killSubst SpecType
spect
       Var -> Annot SpecType -> State CGInfo ()
addIdA Var
x (Bool -> SpecType -> Annot SpecType
forall t. Bool -> t -> Annot t
defAnn Bool
isRec SpecType
spect)
       Template SpecType -> StateT CGInfo Identity (Template SpecType)
forall (m :: * -> *) a. Monad m => a -> m a
return (Template SpecType -> StateT CGInfo Identity (Template SpecType))
-> Template SpecType -> StateT CGInfo Identity (Template SpecType)
forall a b. (a -> b) -> a -> b
$ SpecType -> Template SpecType
forall a. a -> Template a
Asserted SpecType
spect

consBind Bool
isRec CGEnv
γ (Var
x, CoreExpr
e, Internal SpecType
spect)
  = do let γ' :: CGEnv
γ'       = CGEnv
γ CGEnv -> Var -> CGEnv
`setBind` Var
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 :: Maybe (TError SpecType)
cerr = TError SpecType -> Maybe (TError SpecType)
forall a. a -> Maybe a
Just (TError SpecType -> Maybe (TError SpecType))
-> TError SpecType -> Maybe (TError SpecType)
forall a b. (a -> b) -> a -> b
$ SrcSpan -> Doc -> Doc -> TError SpecType
forall t. SrcSpan -> Doc -> Doc -> TError t
ErrHMeas (CGEnv -> SrcSpan
getLocation CGEnv
γπ) (Var -> Doc
forall a. PPrint a => a -> Doc
pprint Var
x) (String -> Doc
text String
forall p. IsString p => p
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 (Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
x Symbol -> HEnv -> Bool
`elemHEnv` CGEnv -> HEnv
holes CGEnv
γ) (State CGInfo () -> State CGInfo ())
-> State CGInfo () -> State CGInfo ()
forall a b. (a -> b) -> a -> b
$
         -- have to add the wf constraint here for HOLEs so we have the proper env
         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 (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap RReft -> RReft
killSubst SpecType
spect
       Var -> Annot SpecType -> State CGInfo ()
addIdA Var
x (Bool -> SpecType -> Annot SpecType
forall t. Bool -> t -> Annot t
defAnn Bool
isRec SpecType
spect)
       Template SpecType -> StateT CGInfo Identity (Template SpecType)
forall (m :: * -> *) a. Monad m => a -> m a
return (Template SpecType -> StateT CGInfo Identity (Template SpecType))
-> Template SpecType -> StateT CGInfo Identity (Template SpecType)
forall a b. (a -> b) -> a -> b
$ SpecType -> Template SpecType
forall a. a -> Template a
Internal SpecType
spect
  where
    explanation :: p
explanation = p
"Cannot give singleton type to the function definition."

consBind Bool
isRec CGEnv
γ (Var
x, CoreExpr
e, Assumed SpecType
spect)
  = do let γ' :: CGEnv
γ' = CGEnv
γ CGEnv -> Var -> CGEnv
`setBind` Var
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
=<< SpecType -> CG SpecType
forall (m :: * -> *) a. Freshable m a => a -> m a
true SpecType
spect
       Var -> Annot SpecType -> State CGInfo ()
addIdA Var
x (Bool -> SpecType -> Annot SpecType
forall t. Bool -> t -> Annot t
defAnn Bool
isRec SpecType
spect)
       Template SpecType -> StateT CGInfo Identity (Template SpecType)
forall (m :: * -> *) a. Monad m => a -> m a
return (Template SpecType -> StateT CGInfo Identity (Template SpecType))
-> Template SpecType -> StateT CGInfo Identity (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
γ (Var
x, CoreExpr
e, Template SpecType
Unknown)
  = do SpecType
t'    <- CGEnv -> CoreExpr -> CG SpecType
consE (CGEnv
γ CGEnv -> Var -> CGEnv
`setBind` Var
x) CoreExpr
e
       SpecType
t     <- Var -> SpecType -> CG SpecType
topSpecType Var
x SpecType
t'
       Var -> Annot SpecType -> State CGInfo ()
addIdA Var
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 (Var -> Bool
isExportedId Var
x) (Var -> SpecType -> State CGInfo ()
forall a. PPrint a => a -> SpecType -> State CGInfo ()
addKuts Var
x SpecType
t)
       Template SpecType -> StateT CGInfo Identity (Template SpecType)
forall (m :: * -> *) a. Monad m => a -> m a
return (Template SpecType -> StateT CGInfo Identity (Template SpecType))
-> Template SpecType -> StateT CGInfo Identity (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 (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 p. Monoid acc => Visitor acc p
kv () ()
  where
    kv :: Visitor acc p
kv    = Visitor acc p
forall acc p. Monoid acc => Visitor acc p
defaultVisitor { txExpr :: p -> Expr -> Expr
txExpr = p -> Expr -> Expr
forall p. p -> Expr -> Expr
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 :: 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 -> (String, Symbol, SpecType) -> CG CGEnv
+= (String
"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 -> (String, Symbol, SpecType) -> CG CGEnv)
-> CGEnv -> [(String, Symbol, SpecType)] -> CG CGEnv
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM CGEnv -> (String, Symbol, SpecType) -> CG CGEnv
(+=) CGEnv
γπ [(String
"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 ())
π]

extender :: F.Symbolic a => CGEnv -> (a, Template SpecType) -> CG CGEnv
extender :: CGEnv -> (a, Template SpecType) -> CG CGEnv
extender CGEnv
γ (a
x, Asserted SpecType
t)
  = case Symbol -> REnv -> Maybe SpecType
lookupREnv (a -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol a
x) (CGEnv -> REnv
assms CGEnv
γ) of
      Just SpecType
t' -> CGEnv
γ CGEnv -> (String, Symbol, SpecType) -> CG CGEnv
+= (String
"extender", a -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol a
x, SpecType
t')
      Maybe SpecType
_       -> CGEnv
γ CGEnv -> (String, Symbol, SpecType) -> CG CGEnv
+= (String
"extender", a -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol a
x, SpecType
t)
extender CGEnv
γ (a
x, Assumed SpecType
t)
  = CGEnv
γ CGEnv -> (String, Symbol, SpecType) -> CG CGEnv
+= (String
"extender", a -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol a
x, SpecType
t)
extender CGEnv
γ (a, Template SpecType)
_
  = CGEnv -> CG CGEnv
forall (m :: * -> *) a. Monad m => a -> m a
return CGEnv
γ

data Template a
  = Asserted a
  | Assumed a
  | Internal a
  | Unknown
  deriving (a -> Template b -> Template a
(a -> b) -> Template a -> Template b
(forall a b. (a -> b) -> Template a -> Template b)
-> (forall a b. a -> Template b -> Template a) -> Functor Template
forall a b. a -> Template b -> Template a
forall a b. (a -> b) -> Template a -> Template b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> Template b -> Template a
$c<$ :: forall a b. a -> Template b -> Template a
fmap :: (a -> b) -> Template a -> Template b
$cfmap :: forall a b. (a -> b) -> Template a -> Template b
Functor, Template a -> Bool
(a -> m) -> Template a -> m
(a -> b -> b) -> b -> Template a -> b
(forall m. Monoid m => Template m -> m)
-> (forall m a. Monoid m => (a -> m) -> Template a -> m)
-> (forall m a. Monoid m => (a -> m) -> Template a -> m)
-> (forall a b. (a -> b -> b) -> b -> Template a -> b)
-> (forall a b. (a -> b -> b) -> b -> Template a -> b)
-> (forall b a. (b -> a -> b) -> b -> Template a -> b)
-> (forall b a. (b -> a -> b) -> b -> Template a -> b)
-> (forall a. (a -> a -> a) -> Template a -> a)
-> (forall a. (a -> a -> a) -> Template a -> a)
-> (forall a. Template a -> [a])
-> (forall a. Template a -> Bool)
-> (forall a. Template a -> Int)
-> (forall a. Eq a => a -> Template a -> Bool)
-> (forall a. Ord a => Template a -> a)
-> (forall a. Ord a => Template a -> a)
-> (forall a. Num a => Template a -> a)
-> (forall a. Num a => Template a -> a)
-> Foldable Template
forall a. Eq a => a -> Template a -> Bool
forall a. Num a => Template a -> a
forall a. Ord a => Template a -> a
forall m. Monoid m => Template m -> m
forall a. Template a -> Bool
forall a. Template a -> Int
forall a. Template a -> [a]
forall a. (a -> a -> a) -> Template a -> a
forall m a. Monoid m => (a -> m) -> Template a -> m
forall b a. (b -> a -> b) -> b -> Template a -> b
forall a b. (a -> b -> b) -> b -> Template a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: Template a -> a
$cproduct :: forall a. Num a => Template a -> a
sum :: Template a -> a
$csum :: forall a. Num a => Template a -> a
minimum :: Template a -> a
$cminimum :: forall a. Ord a => Template a -> a
maximum :: Template a -> a
$cmaximum :: forall a. Ord a => Template a -> a
elem :: a -> Template a -> Bool
$celem :: forall a. Eq a => a -> Template a -> Bool
length :: Template a -> Int
$clength :: forall a. Template a -> Int
null :: Template a -> Bool
$cnull :: forall a. Template a -> Bool
toList :: Template a -> [a]
$ctoList :: forall a. Template a -> [a]
foldl1 :: (a -> a -> a) -> Template a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Template a -> a
foldr1 :: (a -> a -> a) -> Template a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> Template a -> a
foldl' :: (b -> a -> b) -> b -> Template a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Template a -> b
foldl :: (b -> a -> b) -> b -> Template a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Template a -> b
foldr' :: (a -> b -> b) -> b -> Template a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Template a -> b
foldr :: (a -> b -> b) -> b -> Template a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> Template a -> b
foldMap' :: (a -> m) -> Template a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Template a -> m
foldMap :: (a -> m) -> Template a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Template a -> m
fold :: Template m -> m
$cfold :: forall m. Monoid m => Template m -> m
F.Foldable, Functor Template
Foldable Template
Functor Template
-> Foldable Template
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Template a -> f (Template b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    Template (f a) -> f (Template a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Template a -> m (Template b))
-> (forall (m :: * -> *) a.
    Monad m =>
    Template (m a) -> m (Template a))
-> Traversable Template
(a -> f b) -> Template a -> f (Template b)
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => Template (m a) -> m (Template a)
forall (f :: * -> *) a.
Applicative f =>
Template (f a) -> f (Template a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Template a -> m (Template b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Template a -> f (Template b)
sequence :: Template (m a) -> m (Template a)
$csequence :: forall (m :: * -> *) a. Monad m => Template (m a) -> m (Template a)
mapM :: (a -> m b) -> Template a -> m (Template b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Template a -> m (Template b)
sequenceA :: Template (f a) -> f (Template a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
Template (f a) -> f (Template a)
traverse :: (a -> f b) -> Template a -> f (Template b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Template a -> f (Template b)
$cp2Traversable :: Foldable Template
$cp1Traversable :: Functor Template
T.Traversable)

deriving instance (Show a) => (Show (Template a))

instance PPrint a => PPrint (Template a) where
  pprintTidy :: Tidy -> Template a -> Doc
pprintTidy Tidy
k (Asserted a
t) = Doc
"Asserted" Doc -> Doc -> Doc
<+> Tidy -> a -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k a
t
  pprintTidy Tidy
k (Assumed  a
t) = Doc
"Assumed"  Doc -> Doc -> Doc
<+> Tidy -> a -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k a
t
  pprintTidy Tidy
k (Internal a
t) = Doc
"Internal" Doc -> Doc -> Doc
<+> Tidy -> a -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k a
t
  pprintTidy Tidy
_ Template a
Unknown      = Doc
"Unknown"

unTemplate :: Template t -> t
unTemplate :: Template t -> t
unTemplate (Asserted t
t) = t
t
unTemplate (Assumed t
t)  = t
t
unTemplate (Internal t
t) = t
t
unTemplate Template t
_            = Maybe SrcSpan -> String -> t
forall a. Maybe SrcSpan -> String -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing String
"Constraint.Generate.unTemplate called on `Unknown`"

addPostTemplate :: CGEnv
                -> Template SpecType
                -> CG (Template SpecType)
addPostTemplate :: CGEnv
-> Template SpecType -> StateT CGInfo Identity (Template SpecType)
addPostTemplate CGEnv
γ (Asserted SpecType
t) = SpecType -> Template SpecType
forall a. a -> Template a
Asserted (SpecType -> Template SpecType)
-> CG SpecType -> StateT CGInfo Identity (Template SpecType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CGEnv -> SpecType -> CG SpecType
addPost CGEnv
γ SpecType
t
addPostTemplate CGEnv
γ (Assumed  SpecType
t) = SpecType -> Template SpecType
forall a. a -> Template a
Assumed  (SpecType -> Template SpecType)
-> CG SpecType -> StateT CGInfo Identity (Template SpecType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CGEnv -> SpecType -> CG SpecType
addPost CGEnv
γ SpecType
t
addPostTemplate CGEnv
γ (Internal SpecType
t) = SpecType -> Template SpecType
forall a. a -> Template a
Internal  (SpecType -> Template SpecType)
-> CG SpecType -> StateT CGInfo Identity (Template SpecType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CGEnv -> SpecType -> CG SpecType
addPost CGEnv
γ SpecType
t
addPostTemplate CGEnv
_ Template SpecType
Unknown      = Template SpecType -> StateT CGInfo Identity (Template SpecType)
forall (m :: * -> *) a. Monad m => a -> m a
return Template SpecType
forall a. Template a
Unknown

safeFromAsserted :: [Char] -> Template t -> t
safeFromAsserted :: String -> Template t -> t
safeFromAsserted String
_ (Asserted t
t) = t
t
safeFromAsserted String
msg Template t
_ = Maybe SrcSpan -> String -> t
forall a. Maybe SrcSpan -> String -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing (String -> t) -> String -> t
forall a b. (a -> b) -> a -> b
$ String
"safeFromAsserted:" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
msg

-- | @varTemplate@ is only called with a `Just e` argument when the `e`
-- corresponds to the body of a @Rec@ binder.
varTemplate :: CGEnv -> (Var, Maybe CoreExpr) -> CG (Template SpecType)
varTemplate :: CGEnv
-> (Var, Maybe CoreExpr)
-> StateT CGInfo Identity (Template SpecType)
varTemplate CGEnv
γ (Var
x, Maybe CoreExpr
eo) = CGEnv
-> (Var, Maybe CoreExpr)
-> StateT CGInfo Identity (Template SpecType)
varTemplate' CGEnv
γ (Var
x, Maybe CoreExpr
eo) StateT CGInfo Identity (Template SpecType)
-> (Template SpecType
    -> StateT CGInfo Identity (Template SpecType))
-> StateT CGInfo Identity (Template SpecType)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (SpecType -> CG SpecType)
-> Template SpecType -> StateT CGInfo Identity (Template SpecType)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Var -> SpecType -> CG SpecType
topSpecType Var
x)

-- | @lazVarTemplate@ is like `varTemplate` but for binders that are *not*
--   termination checked and hence, the top-level refinement / KVar is
--   stripped out. e.g. see tests/neg/T743.hs
-- varTemplate :: CGEnv -> (Var, Maybe CoreExpr) -> CG (Template SpecType)
-- lazyVarTemplate γ (x, eo) = dbg <$> (topRTypeBase <$>) <$> varTemplate' γ (x, eo)
--   where
--    dbg   = traceShow ("LAZYVAR-TEMPLATE: " ++ show x)

varTemplate' :: CGEnv -> (Var, Maybe CoreExpr) -> CG (Template SpecType)
varTemplate' :: CGEnv
-> (Var, Maybe CoreExpr)
-> StateT CGInfo Identity (Template SpecType)
varTemplate' CGEnv
γ (Var
x, Maybe CoreExpr
eo)
  = case (Maybe CoreExpr
eo, Symbol -> REnv -> Maybe SpecType
lookupREnv (Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
x) (CGEnv -> REnv
grtys CGEnv
γ), Symbol -> REnv -> Maybe SpecType
lookupREnv (Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
x) (CGEnv -> REnv
assms CGEnv
γ), Symbol -> REnv -> Maybe SpecType
lookupREnv (Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
x) (CGEnv -> REnv
intys CGEnv
γ)) of
      (Maybe CoreExpr
_, Just SpecType
t, Maybe SpecType
_, Maybe SpecType
_) -> SpecType -> Template SpecType
forall a. a -> Template a
Asserted (SpecType -> Template SpecType)
-> CG SpecType -> StateT CGInfo Identity (Template SpecType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Var, SpecType) -> CG SpecType
refreshArgsTop (Var
x, SpecType
t)
      (Maybe CoreExpr
_, Maybe SpecType
_, Maybe SpecType
_, Just SpecType
t) -> SpecType -> Template SpecType
forall a. a -> Template a
Internal (SpecType -> Template SpecType)
-> CG SpecType -> StateT CGInfo Identity (Template SpecType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Var, SpecType) -> CG SpecType
refreshArgsTop (Var
x, SpecType
t)
      (Maybe CoreExpr
_, Maybe SpecType
_, Just SpecType
t, Maybe SpecType
_) -> SpecType -> Template SpecType
forall a. a -> Template a
Assumed  (SpecType -> Template SpecType)
-> CG SpecType -> StateT CGInfo Identity (Template SpecType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Var, SpecType) -> CG SpecType
refreshArgsTop (Var
x, SpecType
t)
      (Just CoreExpr
e, Maybe SpecType
_, Maybe SpecType
_, Maybe SpecType
_) -> do SpecType
t  <- KVKind -> CoreExpr -> Type -> CG SpecType
freshTy_expr (Var -> KVKind
RecBindE Var
x) CoreExpr
e (CoreExpr -> Type
exprType CoreExpr
e)
                              WfC -> State CGInfo ()
addW (CGEnv -> SpecType -> WfC
WfC CGEnv
γ SpecType
t)
                              SpecType -> Template SpecType
forall a. a -> Template a
Asserted (SpecType -> Template SpecType)
-> CG SpecType -> StateT CGInfo Identity (Template SpecType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Var, SpecType) -> CG SpecType
refreshArgsTop (Var
x, SpecType
t)
      (Maybe CoreExpr
_,      Maybe SpecType
_, Maybe SpecType
_, Maybe SpecType
_) -> Template SpecType -> StateT CGInfo Identity (Template SpecType)
forall (m :: * -> *) a. Monad m => a -> m a
return Template SpecType
forall a. Template a
Unknown

-- | @topSpecType@ strips out the top-level refinement of "derived var"
topSpecType :: Var -> SpecType -> CG SpecType
topSpecType :: Var -> SpecType -> CG SpecType
topSpecType Var
x SpecType
t = do
  TargetInfo
info  <- CGInfo -> TargetInfo
ghcI (CGInfo -> TargetInfo)
-> StateT CGInfo Identity CGInfo
-> StateT CGInfo Identity TargetInfo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT CGInfo Identity CGInfo
forall s (m :: * -> *). MonadState s m => m s
get
  SpecType -> CG SpecType
forall (m :: * -> *) a. Monad m => a -> m a
return (SpecType -> CG SpecType) -> SpecType -> CG SpecType
forall a b. (a -> b) -> a -> b
$ if TargetSrc -> Var -> Bool
derivedVar (TargetInfo -> TargetSrc
giSrc TargetInfo
info) Var
x then SpecType -> SpecType
forall r c tv. Reftable r => RType c tv r -> RType c tv r
topRTypeBase SpecType
t else SpecType
t

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

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

  | Just (Rs.PatSelfRecBind Var
x CoreExpr
e') <- CoreExpr -> Maybe Pattern
Rs.lift CoreExpr
e
  = let γ' :: CGEnv
γ' = CGEnv
γ { grtys :: REnv
grtys = Symbol -> SpecType -> REnv -> REnv
insertREnv (Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
x) SpecType
t (CGEnv -> REnv
grtys CGEnv
γ)}
    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
γ' ([(Var, CoreExpr)] -> CoreBind
forall b. [(b, Expr b)] -> Bind b
Rec [(Var
x, CoreExpr
e')])

cconsE' CGEnv
γ e :: CoreExpr
e@(Let b :: CoreBind
b@(NonRec Var
x CoreExpr
_) CoreExpr
ee) SpecType
t
  = do HashSet Var
sp <- CGInfo -> HashSet Var
specLVars (CGInfo -> HashSet Var)
-> StateT CGInfo Identity CGInfo
-> StateT CGInfo Identity (HashSet Var)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT CGInfo Identity CGInfo
forall s (m :: * -> *). MonadState s m => m s
get
       if (Var
x Var -> HashSet Var -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`S.member` HashSet Var
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'') = SpecType -> ([[(Symbol, SpecType)]], SpecType)
forall c tv r.
TyConable c =>
RType c tv r -> ([[(Symbol, RType c tv r)]], RType c tv r)
splitConstraints SpecType
t'
    γ' :: CGEnv
γ'         = (CGEnv -> [(Symbol, SpecType)] -> CGEnv)
-> CGEnv -> [[(Symbol, SpecType)]] -> CGEnv
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' CGEnv -> [(Symbol, SpecType)] -> CGEnv
addConstraints CGEnv
γ [[(Symbol, SpecType)]]
css

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

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

cconsE' CGEnv
γ (Lam Var
α CoreExpr
e) (RAllT RTVar RTyVar (RType RTyCon RTyVar ())
α' SpecType
t RReft
r) | Var -> Bool
isTyVar Var
α
  = do CGEnv
γ' <- CGEnv -> Var -> CG CGEnv
updateEnvironment CGEnv
γ Var
α
       CGEnv -> Var -> CoreExpr -> SpecType -> State CGInfo ()
addForAllConstraint CGEnv
γ' Var
α 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
subsTyVar_meet' (RTVar RTyVar (RType RTyCon RTyVar ()) -> RTyVar
forall tv s. RTVar tv s -> tv
ty_var_value RTVar RTyVar (RType RTyCon RTyVar ())
α', Var -> SpecType
forall r c. Monoid r => Var -> RType c RTyVar r
rVar Var
α) SpecType
t

cconsE' CGEnv
γ (Lam Var
x CoreExpr
e) (RFun Symbol
y SpecType
ty SpecType
t RReft
r)
  | Bool -> Bool
not (Var -> Bool
isTyVar Var
x)
  = do CGEnv
γ' <- CGEnv
γ CGEnv -> (String, Symbol, SpecType) -> CG CGEnv
+= (String
"cconsE", Symbol
x', SpecType
ty)
       CGEnv -> CoreExpr -> SpecType -> State CGInfo ()
cconsE CGEnv
γ' CoreExpr
e SpecType
t'
       CGEnv -> Var -> CoreExpr -> SpecType -> State CGInfo ()
addFunctionConstraint CGEnv
γ Var
x CoreExpr
e (Symbol -> SpecType -> SpecType -> RReft -> SpecType
forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
x' SpecType
ty SpecType
t' RReft
r')
       Var -> Annot SpecType -> State CGInfo ()
addIdA Var
x (SpecType -> Annot SpecType
forall t. t -> Annot t
AnnDef SpecType
ty)
  where
    x' :: Symbol
x'  = Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
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 Tickish Var
tt CoreExpr
e) SpecType
t
  = CGEnv -> CoreExpr -> SpecType -> State CGInfo ()
cconsE (CGEnv
γ CGEnv -> Span -> CGEnv
`setLocation` (Tickish Var -> Span
Sp.Tick Tickish Var
tt)) CoreExpr
e SpecType
t

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

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

cconsE' CGEnv
γ (Var Var
x) SpecType
t | Var -> Bool
isHoleVar Var
x Bool -> Bool -> Bool
&& Config -> Bool
typedHoles (CGEnv -> Config
forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)
  = Var -> SpecType -> CGEnv -> State CGInfo ()
addHole Var
x SpecType
t CGEnv
γ 

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 (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= CGEnv -> SpecType -> CG SpecType
addPost CGEnv
γ
        SubC -> String -> State CGInfo ()
addC (CGEnv -> SpecType -> SpecType -> SubC
SubC CGEnv
γ SpecType
te' SpecType
t) (String
"cconsE: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n t = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SpecType -> String
forall a. PPrint a => a -> String
showpp SpecType
t String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n te = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SpecType -> String
forall a. PPrint a => a -> String
showpp SpecType
te String -> String -> String
forall a. [a] -> [a] -> [a]
++ CoreExpr -> String
forall a. Outputable a => a -> String
GM.showPpr CoreExpr
e)

lambdaSingleton :: CGEnv -> F.TCEmb TyCon -> Var -> CoreExpr -> UReft F.Reft
lambdaSingleton :: CGEnv -> TCEmb TyCon -> Var -> CoreExpr -> RReft
lambdaSingleton CGEnv
γ TCEmb TyCon
tce Var
x CoreExpr
e
  | CGEnv -> Bool
forall a. HasConfig a => a -> Bool
higherOrderFlag CGEnv
γ, Just Expr
e' <- CGEnv -> CoreExpr -> Maybe Expr
lamExpr CGEnv
γ CoreExpr
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 (Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
x, Sort
sx) Expr
e'
  where
    sx :: Sort
sx = TCEmb TyCon -> Type -> Sort
typeSort TCEmb TyCon
tce (Type -> Sort) -> Type -> Sort
forall a b. (a -> b) -> a -> b
$ Type -> Type
Ghc.expandTypeSynonyms (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Var -> Type
varType Var
x
lambdaSingleton CGEnv
_ TCEmb TyCon
_ Var
_ CoreExpr
_
  = RReft
forall a. Monoid a => a
mempty

addForAllConstraint :: CGEnv -> Var -> CoreExpr -> SpecType -> CG ()
addForAllConstraint :: CGEnv -> Var -> CoreExpr -> SpecType -> State CGInfo ()
addForAllConstraint CGEnv
γ Var
_ CoreExpr
_ (RAllT RTVar RTyVar (RType RTyCon RTyVar ())
a SpecType
t RReft
r)
  | RReft -> Bool
forall r. Reftable r => r -> Bool
F.isTauto RReft
r 
  = () -> State CGInfo ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  | Bool
otherwise
  = do SpecType
t'       <- SpecType -> CG SpecType
forall (m :: * -> *) a. Freshable m a => a -> m a
true SpecType
t
       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 ())
a (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 -> String -> 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) String
"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
γ Var
_ CoreExpr
_ SpecType
_
  = Maybe SrcSpan -> String -> State CGInfo ()
forall a. Maybe SrcSpan -> String -> 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
γ) String
"addFunctionConstraint: called on non function argument"

  
addFunctionConstraint :: CGEnv -> Var -> CoreExpr -> SpecType -> CG ()
addFunctionConstraint :: CGEnv -> Var -> CoreExpr -> SpecType -> State CGInfo ()
addFunctionConstraint CGEnv
γ Var
x CoreExpr
e (RFun Symbol
y SpecType
ty SpecType
t RReft
r)
  = do SpecType
ty'      <- SpecType -> CG SpecType
forall (m :: * -> *) a. Freshable m a => a -> m a
true SpecType
ty
       SpecType
t'       <- SpecType -> CG SpecType
forall (m :: * -> *) a. Freshable m a => a -> m a
true SpecType
t
       let truet :: RReft -> SpecType
truet = Symbol -> SpecType -> SpecType -> RReft -> SpecType
forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
y SpecType
ty' SpecType
t'
       case (CGEnv -> CoreExpr -> Maybe Expr
lamExpr CGEnv
γ CoreExpr
e, CGEnv -> Bool
forall a. HasConfig a => a -> Bool
higherOrderFlag CGEnv
γ) of
          (Just Expr
e', Bool
True) -> do TCEmb TyCon
tce    <- CGInfo -> TCEmb TyCon
tyConEmbed (CGInfo -> TCEmb TyCon)
-> StateT CGInfo Identity CGInfo
-> StateT CGInfo Identity (TCEmb TyCon)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT CGInfo Identity CGInfo
forall s (m :: * -> *). MonadState s m => m s
get
                                let sx :: Sort
sx  = TCEmb TyCon -> Type -> Sort
typeSort TCEmb TyCon
tce (Type -> Sort) -> Type -> Sort
forall a b. (a -> b) -> a -> b
$ Var -> Type
varType Var
x
                                let ref :: 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 (Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
x, Sort
sx) Expr
e'
                                SubC -> String -> 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)    String
"function constraint singleton"
          (Maybe Expr, Bool)
_ -> SubC -> String -> 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) String
"function constraint true"
addFunctionConstraint CGEnv
γ Var
_ CoreExpr
_ SpecType
_
  = Maybe SrcSpan -> String -> State CGInfo ()
forall a. Maybe SrcSpan -> String -> 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
γ) String
"addFunctionConstraint: called on non function argument"

splitConstraints :: TyConable c
                 => RType c tv r -> ([[(F.Symbol, RType c tv r)]], RType c tv r)
splitConstraints :: RType c tv r -> ([[(Symbol, RType c tv r)]], RType c tv r)
splitConstraints (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') = RType c tv r -> ([[(Symbol, RType c tv r)]], RType c tv r)
forall c tv r.
TyConable c =>
RType c tv r -> ([[(Symbol, RType c tv r)]], RType c tv r)
splitConstraints 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 (RFun Symbol
x 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
isClass c
c
  = let ([[(Symbol, RType c tv r)]]
css, RType c tv r
t') = RType c tv r -> ([[(Symbol, RType c tv r)]], RType c tv r)
forall c tv r.
TyConable c =>
RType c tv r -> ([[(Symbol, RType c tv r)]], RType c tv r)
splitConstraints RType c tv r
t in ([[(Symbol, RType c tv r)]]
css, Symbol -> RType c tv r -> RType c tv r -> r -> RType c tv r
forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
x RType c tv r
tx RType c tv r
t' r
r)
splitConstraints RType c tv r
t
  = ([], RType c tv r
t)

-------------------------------------------------------------------
-- | @instantiateGhosts@ peels away implicit argument binders,
-- instantiates them with fresh variables, and adds those variables
-- to the context as @ebind@s TODO: the second half
-------------------------------------------------------------------
instantiateGhosts :: CGEnv
                 -> SpecType
                 -> CG (Bool, CGEnv, SpecType)
instantiateGhosts :: CGEnv -> SpecType -> CG (Bool, CGEnv, SpecType)
instantiateGhosts CGEnv
γ SpecType
t | Bool -> Bool
not ([(Symbol, SpecType)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Symbol, SpecType)]
yts)
  = do [Symbol]
ys' <- (Symbol -> StateT CGInfo Identity Symbol)
-> [Symbol] -> StateT CGInfo Identity [Symbol]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (StateT CGInfo Identity Symbol
-> Symbol -> StateT CGInfo Identity Symbol
forall a b. a -> b -> a
const StateT CGInfo Identity Symbol
forall (m :: * -> *) a. Freshable m a => m a
fresh) [Symbol]
ys
       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, SpecType) -> CG CGEnv
addEEnv CGEnv
γ ([Symbol] -> [SpecType] -> [(Symbol, SpecType)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
ys' [SpecType]
ts)

       let su :: Subst
su = [(Symbol, Expr)] -> Subst
F.mkSubst ([(Symbol, Expr)] -> Subst) -> [(Symbol, Expr)] -> Subst
forall a b. (a -> b) -> a -> b
$ [Symbol] -> [Expr] -> [(Symbol, Expr)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
ys (Symbol -> Expr
F.EVar (Symbol -> Expr) -> [Symbol] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
ys')
       (Bool, CGEnv, SpecType) -> CG (Bool, CGEnv, SpecType)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, CGEnv
γ', Subst -> SpecType -> SpecType
forall a. Subable a => Subst -> a -> a
F.subst Subst
su SpecType
te')
  where ([(Symbol, SpecType)]
yts, SpecType
te') = SpecType -> ([(Symbol, SpecType)], SpecType)
forall c tv r.
RType c tv r -> ([(Symbol, RType c tv r)], RType c tv r)
bkImplicit SpecType
t
        ([Symbol]
ys, [SpecType]
ts)   = [(Symbol, SpecType)] -> ([Symbol], [SpecType])
forall a b. [(a, b)] -> ([a], [b])
unzip [(Symbol, SpecType)]
yts

instantiateGhosts CGEnv
γ SpecType
t = (Bool, CGEnv, SpecType) -> CG (Bool, CGEnv, SpecType)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, CGEnv
γ, SpecType
t)

bkImplicit :: RType c tv r
           -> ( [(F.Symbol, RType c tv r)]
              , RType c tv r)
bkImplicit :: RType c tv r -> ([(Symbol, RType c tv r)], RType c tv r)
bkImplicit (RImpF Symbol
x RType c tv r
tx RType c tv r
t r
_) = ((Symbol
x,RType c tv r
tx)(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)]
acc, RType c tv r
t')
  where ([(Symbol, RType c tv r)]
acc,RType c tv r
t') = RType c tv r -> ([(Symbol, RType c tv r)], RType c tv r)
forall c tv r.
RType c tv r -> ([(Symbol, RType c tv r)], RType c tv r)
bkImplicit RType c tv r
t
bkImplicit RType c tv r
t = ([],RType c tv r
t)

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

instantiatePreds CGEnv
_ CoreExpr
_ SpecType
t0
  = SpecType -> CG SpecType
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 Var
x CoreExpr
ex) CoreExpr
e) SpecType
t
  = do SpecType
tx <- Type -> CG SpecType
trueTy (Var -> Type
varType Var
x)
       CGEnv
γ' <- (CGEnv
γ, String
"Let NonRec") (CGEnv, String) -> (Symbol, CoreExpr, SpecType) -> CG CGEnv
+++= (Symbol
x', CoreExpr
ex, SpecType
tx)
       CGEnv -> CoreExpr -> SpecType -> State CGInfo ()
cconsE CGEnv
γ' CoreExpr
e SpecType
t
    where
       x' :: Symbol
x' = Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
x

cconsLazyLet CGEnv
_ CoreExpr
_ SpecType
_
  = Maybe SrcSpan -> String -> State CGInfo ()
forall a. Maybe SrcSpan -> String -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing String
"Constraint.Generate.cconsLazyLet called on invalid inputs"

--------------------------------------------------------------------------------
-- | Bidirectional Constraint Generation: SYNTHESIS ----------------------------
--------------------------------------------------------------------------------
consE :: CGEnv -> CoreExpr -> CG SpecType
--------------------------------------------------------------------------------
consE :: CGEnv -> CoreExpr -> CG SpecType
consE CGEnv
γ CoreExpr
e
  | CGEnv -> Bool
forall a. HasConfig a => a -> Bool
patternFlag CGEnv
γ
  , Just Pattern
p <- CoreExpr -> Maybe Pattern
Rs.lift CoreExpr
e
  = CGEnv -> Pattern -> Type -> CG SpecType
consPattern CGEnv
γ (String -> Pattern -> Pattern
forall a. PPrint a => String -> a -> a
F.notracepp String
"CONSE-PATTERN: " Pattern
p) (CoreExpr -> Type
exprType CoreExpr
e)

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

-- [NOTE: PLE-OPT] We *disable* refined instantiation for 
-- reflected functions inside proofs.
consE CGEnv
γ (Var Var
x)
  = do SpecType
t <- (?callStack::CallStack) => CGEnv -> Var -> CG SpecType
CGEnv -> Var -> CG SpecType
varRefType CGEnv
γ Var
x
       Maybe Var -> SrcSpan -> Annot SpecType -> State CGInfo ()
addLocA (Var -> Maybe Var
forall a. a -> Maybe a
Just Var
x) (CGEnv -> SrcSpan
getLocation CGEnv
γ) (CGEnv -> Var -> SpecType -> Annot SpecType
forall t. CGEnv -> Var -> t -> Annot t
varAnn CGEnv
γ Var
x SpecType
t)
       SpecType -> CG SpecType
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
_ <- (String, CoreExpr) -> CGEnv -> SpecType -> SpecType
forall a.
Outputable a =>
(String, a) -> CGEnv -> SpecType -> SpecType
checkAll (String
"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 KVKind -> CoreExpr -> Type -> CG SpecType
freshTy_type KVKind
TypeInstE CoreExpr
e Type
τ 
                         else Type -> CG SpecType
trueTy 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
subsTyVar_meet' (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
       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 -> CG SpecType
forall (m :: * -> *) a. Monad m => a -> m a
return (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
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 -> CG SpecType
forall (m :: * -> *) a. Monad m => a -> m a
return 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 Var
aDict <- CGEnv -> CoreExpr -> Maybe Var
getExprDict CGEnv
γ CoreExpr
a
  = case Maybe (HashMap Symbol (RISig SpecType))
-> Var -> Maybe (RISig SpecType)
forall a1 a.
(Symbolic a1, Show a) =>
Maybe (HashMap Symbol a) -> a1 -> Maybe a
dhasinfo (DEnv Var SpecType -> Var -> Maybe (HashMap Symbol (RISig SpecType))
forall k t.
(Eq k, Hashable k) =>
DEnv k t -> k -> Maybe (HashMap Symbol (RISig t))
dlookup (CGEnv -> DEnv Var SpecType
denv CGEnv
γ) Var
aDict) (CGEnv -> CoreExpr -> Var
getExprFun CGEnv
γ CoreExpr
e) of
      Just RISig SpecType
riSig -> SpecType -> CG SpecType
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 (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 {- πs -}  (CoreExpr -> Maybe SrcSpan
exprLoc CoreExpr
e) SpecType
te''
        let RFun Symbol
x SpecType
tx SpecType
t RReft
_ = (String, CoreExpr) -> CGEnv -> SpecType -> SpecType
forall a.
Outputable a =>
(String, a) -> CGEnv -> SpecType -> SpecType
checkFun (String
"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
γ ({- GM.tracePpr ("APP-EXPR: " ++ GM.showPpr (exprType e)) -} 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 (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''
       (Bool
hasGhost, CGEnv
γ'', SpecType
te''')     <- CGEnv -> SpecType -> CG (Bool, CGEnv, SpecType)
instantiateGhosts CGEnv
γ' SpecType
te''
       let RFun Symbol
x SpecType
tx SpecType
t RReft
_ = (String, CoreExpr) -> CGEnv -> SpecType -> SpecType
forall a.
Outputable a =>
(String, a) -> CGEnv -> SpecType -> SpecType
checkFun (String
"Non-fun App with caller ", CoreExpr
e') CGEnv
γ SpecType
te'''
       CGEnv -> CoreExpr -> SpecType -> State CGInfo ()
cconsE CGEnv
γ'' CoreExpr
a SpecType
tx
       SpecType
tout <- 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 -> 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 -> Maybe Expr) -> CoreExpr -> Maybe Expr
forall a b. (a -> b) -> a -> b
$ CoreExpr -> CoreExpr
simplify CoreExpr
a))
       if Bool
hasGhost
          then do
           SpecType
tk   <- KVKind -> CoreExpr -> Type -> CG SpecType
freshTy_type KVKind
ImplictE CoreExpr
e' (Type -> CG SpecType) -> Type -> CG SpecType
forall a b. (a -> b) -> a -> b
$ 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
tk
           SubC -> String -> State CGInfo ()
addC (CGEnv -> SpecType -> SpecType -> SubC
SubC CGEnv
γ'' SpecType
tout SpecType
tk) String
""
           SpecType -> CG SpecType
forall (m :: * -> *) a. Monad m => a -> m a
return SpecType
tk
          else SpecType -> CG SpecType
forall (m :: * -> *) a. Monad m => a -> m a
return SpecType
tout

consE CGEnv
γ (Lam Var
α CoreExpr
e) | Var -> Bool
isTyVar Var
α
  = do CGEnv
γ' <- CGEnv -> Var -> CG CGEnv
updateEnvironment CGEnv
γ Var
α
       SpecType
t' <- CGEnv -> CoreExpr -> CG SpecType
consE CGEnv
γ' CoreExpr
e
       SpecType -> CG SpecType
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
$ Var -> RTyVar
rTyVar Var
α) SpecType
t' RReft
forall a. Monoid a => a
mempty

consE CGEnv
γ  e :: CoreExpr
e@(Lam Var
x CoreExpr
e1)
  = do SpecType
tx      <- KVKind -> CoreExpr -> Type -> CG SpecType
freshTy_type KVKind
LamE (Var -> CoreExpr
forall b. Var -> Expr b
Var Var
x) Type
τx
       CGEnv
γ'      <- CGEnv
γ CGEnv -> (String, Symbol, SpecType) -> CG CGEnv
+= (String
"consE", Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
x, SpecType
tx)
       SpecType
t1      <- CGEnv -> CoreExpr -> CG SpecType
consE CGEnv
γ' CoreExpr
e1
       Var -> Annot SpecType -> State CGInfo ()
addIdA Var
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
tyConEmbed (CGInfo -> TCEmb TyCon)
-> StateT CGInfo Identity CGInfo
-> StateT CGInfo Identity (TCEmb TyCon)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT CGInfo Identity CGInfo
forall s (m :: * -> *). MonadState s m => m s
get
       SpecType -> CG SpecType
forall (m :: * -> *) a. Monad m => a -> m a
return   (SpecType -> CG SpecType) -> SpecType -> CG SpecType
forall a b. (a -> b) -> a -> b
$ Symbol -> SpecType -> SpecType -> RReft -> SpecType
forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun (Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
x) SpecType
tx SpecType
t1 (RReft -> SpecType) -> RReft -> SpecType
forall a b. (a -> b) -> a -> b
$ CGEnv -> TCEmb TyCon -> Var -> CoreExpr -> RReft
lambdaSingleton CGEnv
γ TCEmb TyCon
tce Var
x CoreExpr
e1
    where
      FunTy { ft_arg :: Type -> Type
ft_arg = Type
τx } = CoreExpr -> Type
exprType CoreExpr
e

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

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

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

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

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

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

consE CGEnv
_ e :: CoreExpr
e@(Coercion Coercion
_)
   = Type -> CG SpecType
trueTy (Type -> CG SpecType) -> Type -> CG SpecType
forall a b. (a -> b) -> a -> b
$ CoreExpr -> Type
exprType CoreExpr
e

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

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

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

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

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

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

subsTyReft :: CGEnv -> RTyVar -> Type -> SpecType -> SpecType 
subsTyReft :: CGEnv -> RTyVar -> Type -> SpecType -> SpecType
subsTyReft CGEnv
γ RTyVar
a Type
t = (Symbol -> 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)]

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

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

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

consPattern :: CGEnv -> Pattern -> Type -> CG SpecType
consPattern CGEnv
γ (Rs.PatBind CoreExpr
e1 Var
x CoreExpr
e2 Type
_ CoreExpr
_ Type
_ Type
_ Var
_) Type
_ = do
  SpecType
tx <- (String, CoreExpr) -> CGEnv -> SpecType -> SpecType
forall a.
Outputable a =>
(String, a) -> CGEnv -> SpecType -> SpecType
checkMonad (String
forall p. IsString p => p
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 -> (String, Symbol, SpecType) -> CG CGEnv
+= (String
"consPattern", Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
x, SpecType
tx)
  Var -> Annot SpecType -> State CGInfo ()
addIdA Var
x (SpecType -> Annot SpecType
forall t. t -> Annot t
AnnDef SpecType
tx)
  SpecType
mt <- CGEnv -> CoreExpr -> CG SpecType
consE CGEnv
γ' CoreExpr
e2
  SpecType -> CG SpecType
forall (m :: * -> *) a. Monad m => a -> m a
return SpecType
mt
  where
    msg :: p
msg = p
"This expression has a refined monadic type; run with --no-pattern-inline: "

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

           G |- e ~> et
    ------------------------
      G |- return e ~ m et
 -}
consPattern CGEnv
γ (Rs.PatReturn CoreExpr
e Type
m CoreExpr
_ Type
_ Var
_) Type
t = do
  SpecType
et    <- String -> SpecType -> SpecType
forall a. PPrint a => String -> a -> a
F.notracepp String
"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    <- Type -> CG SpecType
trueTy  Type
m
  SpecType
tt    <- Type -> CG SpecType
trueTy  Type
t
  SpecType -> CG SpecType
forall (m :: * -> *) a. Monad m => a -> m a
return (SpecType -> SpecType -> SpecType -> SpecType
mkRAppTy SpecType
mt SpecType
et SpecType
tt) -- /// {-    $ RAppTy mt et mempty -}

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

consPattern CGEnv
γ (Rs.PatProject Var
xe Var
_ Type
τ DataCon
c [Var]
ys Int
i) Type
_ = do
  let yi :: Var
yi = [Var]
ys [Var] -> Int -> Var
forall a. [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
<<= KVKind -> CoreExpr -> Type -> CG SpecType
freshTy_type KVKind
ProjectE (Var -> CoreExpr
forall b. Var -> Expr b
Var Var
yi) Type
τ
  CGEnv
γ'   <- CGEnv
-> Var -> [AltCon] -> AltCon -> [Var] -> Maybe [Int] -> CG CGEnv
caseEnv CGEnv
γ Var
xe [] (DataCon -> AltCon
DataAlt DataCon
c) [Var]
ys ([Int] -> Maybe [Int]
forall a. a -> Maybe a
Just [Int
i])
  SpecType
ti   <- {- γ' ??= yi -} (?callStack::CallStack) => CGEnv -> Var -> CG SpecType
CGEnv -> Var -> CG SpecType
varRefType CGEnv
γ' Var
yi
  SubC -> String -> State CGInfo ()
addC (CGEnv -> SpecType -> SpecType -> SubC
SubC CGEnv
γ' SpecType
ti SpecType
t) String
"consPattern:project"
  SpecType -> CG SpecType
forall (m :: * -> *) a. Monad m => a -> m a
return SpecType
t

consPattern CGEnv
γ (Rs.PatSelfBind Var
_ 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 -> 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] -> [SpecProp] -> 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 -> String -> SpecType
forall a. Maybe SrcSpan -> String -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing (String -> SpecType) -> String -> SpecType
forall a b. (a -> b) -> a -> b
$ String
"Unexpected return-pattern" 

checkMonad :: (Outputable a) => (String, a) -> CGEnv -> SpecType -> SpecType
checkMonad :: (String, a) -> CGEnv -> SpecType -> SpecType
checkMonad (String, 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
_)
     | [SpecType] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SpecType]
ts Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 = [SpecType] -> SpecType
forall a. [a] -> a
last [SpecType]
ts
   go (RAppTy SpecType
_ SpecType
t RReft
_) = SpecType
t
   go SpecType
t              = (String, a) -> CGEnv -> SpecType -> SpecType
forall a.
Outputable a =>
(String, a) -> CGEnv -> SpecType -> SpecType
checkErr (String, 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 -> Coercion -> CG SpecType
castTy CGEnv
γ Type
t CoreExpr
e (AxiomInstCo CoAxiom Branched
ca Int
_ [Coercion]
_)
  = 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 (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
_ [Coercion]
_))
  = do Maybe SpecType
mtc <- TyCon -> StateT CGInfo Identity (Maybe SpecType)
lookupNewType (CoAxiom Branched -> TyCon
forall (br :: BranchFlag). CoAxiom br -> TyCon
coAxiomTyCon CoAxiom Branched
ca)
       case Maybe SpecType
mtc of
        Just SpecType
tc -> CGEnv -> CoreExpr -> SpecType -> State CGInfo ()
cconsE CGEnv
γ CoreExpr
e SpecType
tc
        Maybe SpecType
Nothing -> () -> State CGInfo ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
       CGEnv -> Type -> CoreExpr -> CG SpecType
castTy' CGEnv
γ Type
t CoreExpr
e

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


castTy' :: CGEnv -> Type -> CoreExpr -> CG SpecType
castTy' CGEnv
γ Type
τ (Var Var
x)
  = do SpecType
t <- Type -> CG SpecType
trueTy Type
τ
       -- tx <- varRefType γ x -- NV HERE: the refinements of the var x do not get into the 
       --                      -- environment. Check 
       let ce :: Expr
ce = 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
$ Var -> Type
varType Var
x) 
                       (TCEmb TyCon -> Type -> Sort
typeSort (CGEnv -> TCEmb TyCon
emb CGEnv
γ) Type
τ) 
                       (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Var -> Expr
forall a. Expression a => a -> Expr
F.expr Var
x  
       SpecType -> CG SpecType
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 (Reft -> RReft) -> Reft -> RReft
forall a b. (a -> b) -> a -> b
$ Expr -> Reft
forall a. Expression a => a -> Reft
F.uexprReft (Expr -> Reft) -> Expr -> Reft
forall a b. (a -> b) -> a -> b
$ Expr
ce)) {- `F.meet` tx -})
  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 Tickish Var
_ CoreExpr
e)
  = CGEnv -> Type -> CoreExpr -> CG SpecType
castTy' CGEnv
γ Type
t CoreExpr
e

castTy' CGEnv
_ Type
_ CoreExpr
e
  = Maybe SrcSpan -> String -> CG SpecType
forall a. Maybe SrcSpan -> String -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing (String -> CG SpecType) -> String -> CG SpecType
forall a b. (a -> b) -> a -> b
$ String
"castTy cannot handle expr " String -> String -> String
forall a. [a] -> [a] -> [a]
++ CoreExpr -> String
forall a. Outputable a => a -> String
GM.showPpr CoreExpr
e

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

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

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

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

--------------------------------------------------------------------------------
-- | @consFreshE@ is used to *synthesize* types with a **fresh template**.
--   e.g. at joins, recursive binders, polymorphic instantiations etc. It is
--   the "portal" that connects `consE` (synthesis) and `cconsE` (checking)
--------------------------------------------------------------------------------
cconsFreshE :: KVKind -> CGEnv -> CoreExpr -> CG SpecType
cconsFreshE :: KVKind -> CGEnv -> CoreExpr -> CG SpecType
cconsFreshE KVKind
kvkind CGEnv
γ CoreExpr
e = do
  SpecType
t   <- KVKind -> CoreExpr -> Type -> CG SpecType
freshTy_type KVKind
kvkind CoreExpr
e (Type -> CG SpecType) -> Type -> CG SpecType
forall a b. (a -> b) -> a -> b
$ 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 (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 :: 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 -> String -> a
forall a. Maybe SrcSpan -> String -> 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
γ) String
msg
  where
    msg :: String
msg = [String] -> String
unlines [ String
"checkUnbound: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Symbol -> String
forall a. Show a => a -> String
show Symbol
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" is elem of syms of " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
t
                  , String
"In", CoreExpr -> String
forall a. Outputable a => a -> String
GM.showPpr CoreExpr
e, String
"Arg = " , a2 -> String
forall a. Show a => a -> String
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 -> (String, Symbol, SpecType) -> CG CGEnv
+= (String
"dropExists", Symbol
x, SpecType
tx)
dropExists CGEnv
γ SpecType
t            = (CGEnv, SpecType) -> CG (CGEnv, SpecType)
forall (m :: * -> *) a. Monad m => a -> m a
return (CGEnv
γ, SpecType
t)

dropConstraints :: CGEnv -> SpecType -> CG SpecType
dropConstraints :: CGEnv -> SpecType -> CG SpecType
dropConstraints CGEnv
γ (RFun Symbol
x tx :: SpecType
tx@(RApp RTyCon
c [SpecType]
_ [SpecProp]
_ RReft
_) SpecType
t RReft
r) | RTyCon -> Bool
forall c. TyConable c => c -> Bool
isClass RTyCon
c
  = ((SpecType -> RReft -> SpecType) -> RReft -> SpecType -> SpecType
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Symbol -> SpecType -> SpecType -> RReft -> SpecType
forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
x 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
γ SpecType
t
dropConstraints CGEnv
γ (RRTy [(Symbol, SpecType)]
cts RReft
_ Oblig
OCons SpecType
t)
  = 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 -> (String, Symbol, SpecType) -> CG CGEnv
`addSEnv` (String
"splitS", Symbol
x,SpecType
t)) CGEnv
γ [(Symbol, SpecType)]
xts
       SubC -> String -> State CGInfo ()
addC (CGEnv -> SpecType -> SpecType -> SubC
SubC  CGEnv
γ' SpecType
t1 SpecType
t2)  String
"dropConstraints"
       CGEnv -> SpecType -> CG SpecType
dropConstraints CGEnv
γ SpecType
t
  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 (m :: * -> *) a. Monad m => a -> m a
return SpecType
t

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

{- 

case x :: List b of 
  Emp -> e 

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

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

  let (Symbol
x' : [Symbol]
ys')   = Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (Var -> Symbol) -> [Var] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Var
xVar -> [Var] -> [Var]
forall a. a -> [a] -> [a]
:[Var]
ys)
  SpecType
xt0             <- (String, Var) -> CGEnv -> SpecType -> SpecType
forall a.
Outputable a =>
(String, a) -> CGEnv -> SpecType -> SpecType
checkTyCon (String
"checkTycon cconsCase", Var
x) CGEnv
γ (SpecType -> SpecType) -> CG SpecType -> CG SpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CGEnv
γ (?callStack::CallStack) => CGEnv -> Var -> CG SpecType
CGEnv -> Var -> CG SpecType
??= Var
x
  let xt :: SpecType
xt           = 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 -> Var -> CG SpecType
CGEnv -> Var -> CG SpecType
??= (DataCon -> Var
dataConWorkId DataCon
c) CG SpecType -> (SpecType -> CG SpecType) -> CG SpecType
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 -> [Var] -> (SpecType, [SpecType], SpecType)
unfoldR SpecType
tdc SpecType
xt [Var]
ys
  [SpecType]
yts             <- Maybe [Int] -> [SpecType] -> StateT CGInfo Identity [SpecType]
projectTypes Maybe [Int]
pIs [SpecType]
yts'
  let ys'' :: [Symbol]
ys''         = Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (Var -> Symbol) -> [Var] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Var -> Bool) -> [Var] -> [Var]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Var -> Bool) -> Var -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> Bool
GM.isEvVar) [Var]
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          = String -> [Symbol] -> [SpecType] -> [(Symbol, SpecType)]
forall a b.
(?callStack::CallStack) =>
String -> [a] -> [b] -> [(a, b)]
safeZip String
"cconsCase" (Symbol
x'Symbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
:[Symbol]
ys') (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', SpecType
xt)]
  
caseEnv CGEnv
γ Var
x [AltCon]
acs AltCon
a [Var]
_ Maybe [Int]
_ = do 
  let x' :: Symbol
x'  = Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
x
  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 -> Var -> CG SpecType
CGEnv -> Var -> CG SpecType
??= Var
x)
  CGEnv
cγ     <- CGEnv -> Symbol -> [(Symbol, SpecType)] -> CG CGEnv
addBinders CGEnv
γ Symbol
x' [(Symbol
x', SpecType
xt')]
  CGEnv -> CG CGEnv
forall (m :: * -> *) a. Monad m => a -> m a
return CGEnv
cγ

--------------------------------------------------------------------------------
-- | `projectTypes` masks (i.e. true's out) all types EXCEPT those
--   at given indices; it is used to simplify the environment used
--   when projecting out fields of single-ctor datatypes.
--------------------------------------------------------------------------------
projectTypes :: Maybe [Int] -> [SpecType] -> CG [SpecType]
projectTypes :: Maybe [Int] -> [SpecType] -> StateT CGInfo Identity [SpecType]
projectTypes Maybe [Int]
Nothing   [SpecType]
ts = [SpecType] -> StateT CGInfo Identity [SpecType]
forall (m :: * -> *) a. Monad m => a -> m a
return [SpecType]
ts
projectTypes (Just [Int]
is) [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)
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]
is) ([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 (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t a
is       = a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
t
      | Bool
otherwise         = a -> m a
forall (m :: * -> *) a. Freshable m a => a -> m a
true 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 -> String -> Reft
forall a. Maybe SrcSpan -> String -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing String
"Constraint : altReft"

unfoldR :: SpecType -> SpecType -> [Var] -> (SpecType, [SpecType], SpecType)
unfoldR :: SpecType -> SpecType -> [Var] -> (SpecType, [SpecType], SpecType)
unfoldR SpecType
td (RApp RTyCon
_ [SpecType]
ts [SpecProp]
rs RReft
_) [Var]
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 -> [SpecProp] -> SpecType
instantiatePvs (SpecType -> [SpecType] -> SpecType
instantiateTys SpecType
td [SpecType]
ts) ([SpecProp] -> [SpecProp]
forall a. [a] -> [a]
reverse [SpecProp]
rs)
        -- TODO: if we ever want to support applying implicits explicitly, will need to rejigger
        (([Symbol]
_,[SpecType]
_,[RReft]
_),([Symbol]
ys0,[SpecType]
yts',[RReft]
_), SpecType
rt) = SpecType
-> (([Symbol], [SpecType], [RReft]),
    ([Symbol], [SpecType], [RReft]), SpecType)
forall t t1 a.
PPrint (RType t t1 a) =>
RType t t1 a
-> (([Symbol], [RType t t1 a], [a]),
    ([Symbol], [RType t t1 a], [a]), RType t t1 a)
safeBkArrow (String -> SpecType -> SpecType
forall a. PPrint a => String -> a -> a
F.notracepp String
msg (SpecType -> SpecType) -> SpecType -> SpecType
forall a b. (a -> b) -> a -> b
$ SpecType -> [SpecType] -> SpecType
instantiateTys SpecType
tbody [SpecType]
tvs')
        msg :: String
msg                = String
"INST-TY: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (SpecType, [SpecType], SpecType, [Var], [SpecType]) -> String
forall a. PPrint a => a -> String
F.showpp (SpecType
td, [SpecType]
ts, SpecType
tbody, [Var]
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. [a] -> a
last [SpecType]
yts'', [SpecType] -> [SpecType]
forall a. [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'])
        ([Var]
αs, [Symbol]
ys')          = ([Var] -> [Symbol]) -> ([Var], [Var]) -> ([Var], [Symbol])
forall b c a. (b -> c) -> (a, b) -> (a, c)
mapSnd (Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (Var -> Symbol) -> [Var] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) (([Var], [Var]) -> ([Var], [Symbol]))
-> ([Var], [Var]) -> ([Var], [Symbol])
forall a b. (a -> b) -> a -> b
$ (Var -> Bool) -> [Var] -> ([Var], [Var])
forall a. (a -> Bool) -> [a] -> ([a], [a])
L.partition Var -> Bool
isTyVar [Var]
ys
        tvs' :: [SpecType]
        tvs' :: [SpecType]
tvs'               = Var -> SpecType
forall r c. Monoid r => Var -> RType c RTyVar r
rVar (Var -> SpecType) -> [Var] -> [SpecType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Var]
αs
        tvys :: [RRType r]
tvys               = Type -> RRType r
forall r. Monoid r => Type -> RRType r
ofType (Type -> RRType r) -> (Var -> Type) -> Var -> RRType r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> Type
varType (Var -> RRType r) -> [Var] -> [RRType r]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Var]
αs

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

instantiateTys :: SpecType -> [SpecType] -> SpecType
instantiateTys :: SpecType -> [SpecType] -> SpecType
instantiateTys = (SpecType -> SpecType -> SpecType)
-> SpecType -> [SpecType] -> SpecType
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 ())), Eq 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
subsTyVar_meet' (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 -> String -> RType c tv r
forall a. Maybe SrcSpan -> String -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing String
"Constraint.instantiateTy"

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

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

checkFun :: (Outputable a) => (String, a) -> CGEnv -> SpecType -> SpecType
checkFun :: (String, a) -> CGEnv -> SpecType -> SpecType
checkFun (String, a)
_ CGEnv
_ t :: SpecType
t@(RFun Symbol
_ SpecType
_ SpecType
_ RReft
_) = SpecType
t
checkFun (String, a)
x CGEnv
g SpecType
t                = (String, a) -> CGEnv -> SpecType -> SpecType
forall a.
Outputable a =>
(String, a) -> CGEnv -> SpecType -> SpecType
checkErr (String, a)
x CGEnv
g SpecType
t

checkAll :: (Outputable a) => (String, a) -> CGEnv -> SpecType -> SpecType
checkAll :: (String, a) -> CGEnv -> SpecType -> SpecType
checkAll (String, a)
_ CGEnv
_ t :: SpecType
t@(RAllT RTVar RTyVar (RType RTyCon RTyVar ())
_ SpecType
_ RReft
_)  = SpecType
t
checkAll (String, a)
x CGEnv
g SpecType
t                = (String, a) -> CGEnv -> SpecType -> SpecType
forall a.
Outputable a =>
(String, a) -> CGEnv -> SpecType -> SpecType
checkErr (String, a)
x CGEnv
g SpecType
t

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

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

-----------------------------------------------------------------------
-- | Helpers: Creating Fresh Refinement -------------------------------
-----------------------------------------------------------------------
freshPredRef :: CGEnv -> CoreExpr -> PVar RSort -> CG SpecProp
freshPredRef :: CGEnv -> CoreExpr -> PVar (RType RTyCon RTyVar ()) -> CG SpecProp
freshPredRef CGEnv
γ CoreExpr
e (PV Symbol
_ (PVProp RType RTyCon RTyVar ()
τ) Symbol
_ [(RType RTyCon RTyVar (), Symbol, Expr)]
as)
  = do SpecType
t    <- KVKind -> CoreExpr -> Type -> CG SpecType
freshTy_type KVKind
PredInstE CoreExpr
e (RType RTyCon RTyVar () -> Type
forall r. ToTypeable r => RRType r -> Type
toType RType RTyCon RTyVar ()
τ)
       [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)
mapM (\(RType RTyCon RTyVar (), Symbol, Expr)
_ -> 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 -> (String, Symbol, SpecType) -> CG CGEnv)
-> CGEnv -> [(String, Symbol, SpecType)] -> CG CGEnv
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM CGEnv -> (String, Symbol, SpecType) -> CG CGEnv
(+=) CGEnv
γ [(String
"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
       SpecProp -> CG SpecProp
forall (m :: * -> *) a. Monad m => a -> m a
return (SpecProp -> CG SpecProp) -> SpecProp -> CG SpecProp
forall a b. (a -> b) -> a -> b
$ [(Symbol, RType RTyCon RTyVar ())] -> SpecType -> SpecProp
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 -> String -> CG SpecProp
forall a. Maybe SrcSpan -> String -> a
todo Maybe SrcSpan
forall a. Maybe a
Nothing String
"EFFECTS:freshPredRef"


--------------------------------------------------------------------------------
-- | Helpers: Creating Refinement Types For Various Things ---------------------
--------------------------------------------------------------------------------
argType :: Type -> Maybe F.Expr
argType :: Type -> Maybe Expr
argType (LitTy (NumTyLit Integer
i))
  = Integer -> Maybe Expr
mkI Integer
i
argType (LitTy (StrTyLit FastString
s))
  = ByteString -> Maybe Expr
mkS (ByteString -> Maybe Expr) -> ByteString -> Maybe Expr
forall a b. (a -> b) -> a -> b
$ FastString -> ByteString
bytesFS FastString
s
argType (TyVarTy Var
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
$ Var -> Name
varName Var
x
argType Type
t
  | String -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (Type -> String
forall a. Outputable a => a -> String
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 Var
v)     = Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> Maybe Expr) -> Expr -> Maybe Expr
forall a b. (a -> b) -> a -> b
$ Var -> Expr
forall a. Symbolic a => a -> Expr
F.eVar Var
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 Tickish Var
_ 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


-- NIKI TODO: merge arg/lam/fun-Expr
lamExpr :: CGEnv -> CoreExpr -> Maybe F.Expr
lamExpr :: CGEnv -> CoreExpr -> Maybe Expr
lamExpr CGEnv
_ (Var Var
v)     =  Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> Maybe Expr) -> Expr -> Maybe Expr
forall a b. (a -> b) -> a -> b
$ Var -> Expr
forall a. Symbolic a => a -> Expr
F.eVar Var
v
lamExpr 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
lamExpr CGEnv
γ (Tick Tickish Var
_ CoreExpr
e)  = CGEnv -> CoreExpr -> Maybe Expr
lamExpr CGEnv
γ CoreExpr
e
lamExpr CGEnv
γ (App CoreExpr
e (Type Type
_)) = CGEnv -> CoreExpr -> Maybe Expr
lamExpr CGEnv
γ CoreExpr
e
lamExpr CGEnv
γ (App CoreExpr
e1 CoreExpr
e2) = case (CGEnv -> CoreExpr -> Maybe Expr
lamExpr CGEnv
γ CoreExpr
e1, CGEnv -> CoreExpr -> Maybe Expr
lamExpr CGEnv
γ CoreExpr
e2) of
                              (Just Expr
p1, Just Expr
p2) | Bool -> Bool
not (CoreExpr -> Bool
GM.isPredExpr CoreExpr
e2) -- (isClassPred $ exprType e2)
                                                 -> Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> Maybe Expr) -> Expr -> Maybe Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> Expr
F.EApp Expr
p1 Expr
p2
                              (Just Expr
p1, Just Expr
_ ) -> Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
p1
                              (Maybe Expr, Maybe Expr)
_  -> Maybe Expr
forall a. Maybe a
Nothing
lamExpr CGEnv
γ (Let (NonRec Var
x CoreExpr
ex) CoreExpr
e) = case (CGEnv -> CoreExpr -> Maybe Expr
lamExpr CGEnv
γ CoreExpr
ex, CGEnv -> CoreExpr -> Maybe Expr
lamExpr CGEnv
γ CoreExpr
e) of
                                       (Just Expr
px, Just Expr
p) -> Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr
p Expr -> (Symbol, Expr) -> Expr
forall a. Subable a => a -> (Symbol, Expr) -> a
`F.subst1` (Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
x, Expr
px))
                                       (Maybe Expr, Maybe Expr)
_  -> Maybe Expr
forall a. Maybe a
Nothing
lamExpr CGEnv
γ (Lam Var
x CoreExpr
e)   = case CGEnv -> CoreExpr -> Maybe Expr
lamExpr CGEnv
γ CoreExpr
e of
                            Just Expr
p -> Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> Maybe Expr) -> Expr -> Maybe Expr
forall a b. (a -> b) -> a -> b
$ (Symbol, Sort) -> Expr -> Expr
F.ELam (Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
x, TCEmb TyCon -> Type -> Sort
typeSort (CGEnv -> TCEmb TyCon
emb CGEnv
γ) (Type -> Sort) -> Type -> Sort
forall a b. (a -> b) -> a -> b
$ Type -> Type
Ghc.expandTypeSynonyms (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Var -> Type
varType Var
x) Expr
p
                            Maybe Expr
_ -> Maybe Expr
forall a. Maybe a
Nothing
lamExpr CGEnv
_ CoreExpr
_           = Maybe Expr
forall a. Maybe a
Nothing

--------------------------------------------------------------------------------
(??=) :: (?callStack :: CallStack) => CGEnv -> Var -> CG SpecType
--------------------------------------------------------------------------------
CGEnv
γ ??= :: CGEnv -> Var -> CG SpecType
??= Var
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' = Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
x
            tx :: SpecType
tx = SpecType -> Maybe SpecType -> SpecType
forall a. a -> Maybe a -> a
fromMaybe SpecType
forall r. 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
$ Var -> Type
varType Var
x


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

varRefType' :: CGEnv -> Var -> SpecType -> SpecType
varRefType' :: CGEnv -> Var -> SpecType -> SpecType
varRefType' CGEnv
γ Var
x SpecType
t'
  | Just HashMap Symbol SpecType
tys <- CGEnv -> Maybe (HashMap Symbol SpecType)
trec CGEnv
γ, Just SpecType
tr  <- Symbol -> HashMap Symbol SpecType -> Maybe SpecType
forall k v. (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 = Var -> RReft
forall a. Symbolic a => a -> RReft
singletonReft Var
x
    x' :: Symbol
x' = Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
x
    strengthen :: RType c tv r -> r -> RType c tv r
strengthen
      | CGEnv -> Bool
forall a. HasConfig a => a -> Bool
higherOrderFlag CGEnv
γ
      = RType c tv r -> r -> RType c tv r
forall r c tv.
(PPrint r, Reftable r) =>
RType c tv r -> r -> RType c tv r
strengthenMeet
      | Bool
otherwise
      = RType c tv r -> r -> RType c tv r
forall r c tv.
(PPrint r, Reftable r) =>
RType c tv r -> r -> RType c tv r
strengthenTop

-- | create singleton types for function application
makeSingleton :: CGEnv -> CoreExpr -> SpecType -> SpecType
makeSingleton :: CGEnv -> CoreExpr -> SpecType -> SpecType
makeSingleton CGEnv
γ CoreExpr
e SpecType
t
  | CGEnv -> Bool
forall a. HasConfig a => a -> Bool
higherOrderFlag CGEnv
γ, App CoreExpr
f CoreExpr
x <- CoreExpr -> CoreExpr
simplify CoreExpr
e
  = 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 (CoreExpr -> Bool
GM.isPredExpr CoreExpr
x) -- (isClassPred $ exprType x)
                 -> SpecType -> RReft -> SpecType
forall r c tv.
(PPrint r, Reftable r) =>
RType c tv r -> r -> RType c tv r
strengthenMeet SpecType
t (Reft -> RReft
forall r. 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
e) 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 (Reft -> RReft) -> Reft -> RReft
forall a b. (a -> b) -> a -> b
$ 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 Var
x)
      | Config -> Bool
rankNTypes (CGEnv -> Config
forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)
      , Just Expr
e <- Var -> HashMap Var Expr -> Maybe Expr
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup Var
x (CGEnv -> HashMap Var 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 Var
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 (Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
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 (CoreExpr -> Bool
GM.isPredExpr CoreExpr
e2) -- (isClassPred $ exprType 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 Tickish Var
_ 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 Var
x CoreExpr
e) | Var -> Bool
isTyVar Var
x = CoreExpr -> CoreExpr
simplify CoreExpr
e 
simplify CoreExpr
e                = CoreExpr
e


singletonReft :: (F.Symbolic a) => a -> UReft F.Reft
singletonReft :: 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

-- | RJ: `nomeet` replaces `strengthenS` for `strengthen` in the definition
--   of `varRefType`. Why does `tests/neg/strata.hs` fail EVEN if I just replace
--   the `otherwise` case? The fq file holds no answers, both are sat.
strengthenTop :: (PPrint r, F.Reftable r) => RType c tv r -> r -> RType c tv r
strengthenTop :: 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 RType c tv r
t1 RType c tv r
t2 r
r) r
r'  = Symbol -> RType c tv r -> RType c tv r -> r -> RType c tv r
forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
b 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

-- TODO: this is almost identical to RT.strengthen! merge them!
strengthenMeet :: (PPrint r, F.Reftable r) => RType c tv r -> r -> RType c tv r
strengthenMeet :: 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 RType c tv r
t1 RType c tv r
t2 r
r) r
r'  = Symbol -> RType c tv r -> RType c tv r -> r -> RType c tv r
forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
b 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

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

--------------------------------------------------------------------------------
-- | Cleaner Signatures For Rec-bindings ---------------------------------------
--------------------------------------------------------------------------------
exprLoc                         :: CoreExpr -> Maybe SrcSpan
exprLoc :: CoreExpr -> Maybe SrcSpan
exprLoc (Tick Tickish Var
tt CoreExpr
_)             = SrcSpan -> Maybe SrcSpan
forall a. a -> Maybe a
Just (SrcSpan -> Maybe SrcSpan) -> SrcSpan -> Maybe SrcSpan
forall a b. (a -> b) -> a -> b
$ Tickish Var -> SrcSpan
forall a. Outputable a => Tickish a -> SrcSpan
GM.tickSrcSpan Tickish Var
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 (CoreExpr -> Type
exprType CoreExpr
a) Type
predType

-- | @isGenericVar@ determines whether the @RTyVar@ has no class constraints
isGenericVar :: RTyVar -> SpecType -> Bool
isGenericVar :: RTyVar -> SpecType -> Bool
isGenericVar RTyVar
α SpecType
t =  ((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 ()), Eq b, Hashable b) =>
RType RTyCon b r -> [(Class, b)]
classConstrs SpecType
t)
  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 (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name
ordClassName, Name
eqClassName] -- , functorClassName, monadClassName]

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

instance MonadFail Data.Functor.Identity.Identity where 
  fail :: String -> Identity a
fail String
msg = Maybe SrcSpan -> String -> Identity a
forall a. Maybe SrcSpan -> String -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing String
msg