{-# LANGUAGE TupleSections #-}
{-# OPTIONS_GHC -Wno-x-partial #-}
-- | This module defines code for generating termination constraints.

module Language.Haskell.Liquid.Constraint.Termination (
  TCheck(..)
, mkTCheck
, doTermCheck
, makeTermEnvs
, makeDecrIndex
, checkIndex
, recType
, unOCons
, consCBSizedTys
, consCBWithExprs
) where

import           Data.Maybe ( fromJust, catMaybes, mapMaybe )
import qualified Data.List                          as L
import qualified Data.HashSet                       as S
import qualified Data.Traversable                   as T
import qualified Data.HashMap.Strict                as M
import           Control.Monad ( foldM, forM )
import           Control.Monad.State ( gets )
import           Text.PrettyPrint.HughesPJ ( (<+>), text )
import qualified Language.Haskell.Liquid.GHC.Misc                    as GM
import qualified Language.Fixpoint.Types            as F
import           Language.Haskell.Liquid.Constraint.Types (CG, CGInfo (..), CGEnv, makeRecInvariants)
import           Language.Haskell.Liquid.Constraint.Monad (addWarning)
import           Language.Haskell.Liquid.Constraint.Env (setTRec)
import           Language.Haskell.Liquid.Constraint.Template ( Template(..), unTemplate, varTemplate, safeFromAsserted, extender )
import           Language.Haskell.Liquid.Types.Errors
import           Language.Haskell.Liquid.Types.Fresh
import           Language.Haskell.Liquid.Types.RType
import           Language.Haskell.Liquid.Types.RTypeOp
import           Language.Haskell.Liquid.Types.Types
import           Language.Haskell.Liquid.Types.RefType (isDecreasing, makeDecrType, makeLexRefa, makeNumEnv)
import           Language.Haskell.Liquid.Misc (safeFromLeft, replaceN, (<->), zip4, safeFromJust, fst5)
import           Language.Haskell.Liquid.UX.Config
import qualified Liquid.GHC.API as GHC


data TCheck = TerminationCheck | StrataCheck | NoCheck
  deriving Int -> TCheck -> ShowS
[TCheck] -> ShowS
TCheck -> String
(Int -> TCheck -> ShowS)
-> (TCheck -> String) -> ([TCheck] -> ShowS) -> Show TCheck
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> TCheck -> ShowS
showsPrec :: Int -> TCheck -> ShowS
$cshow :: TCheck -> String
show :: TCheck -> String
$cshowList :: [TCheck] -> ShowS
showList :: [TCheck] -> ShowS
Show

mkTCheck :: Bool -> Bool -> TCheck
mkTCheck :: Bool -> Bool -> TCheck
mkTCheck Bool
tc Bool
is
  | Bool -> Bool
not Bool
is    = TCheck
StrataCheck
  | Bool
tc        = TCheck
TerminationCheck
  | Bool
otherwise = TCheck
NoCheck

doTermCheck :: Config -> GHC.Bind GHC.Var -> CG Bool
doTermCheck :: Config -> Bind Var -> CG Bool
doTermCheck Config
cfg Bind Var
bind = do
  lazyVs    <- (CGInfo -> HashSet Var) -> StateT CGInfo Identity (HashSet Var)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CGInfo -> HashSet Var
specLazy
  termVs    <- gets specTmVars
  let 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
nocheck Var
x) [Var]
xs
  let 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 -> HashSet Var -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`S.member` HashSet Var
termVs) [Var]
xs
  return     $ chk && not skip
  where
    nocheck :: Var -> Bool
nocheck  = if Config -> Bool
typeclass Config
cfg then Var -> Bool
GM.isEmbeddedDictVar else Var -> Bool
forall a. Symbolic a => a -> Bool
GM.isInternal
    xs :: [Var]
xs       = Bind Var -> [Var]
forall b. Bind b -> [b]
GHC.bindersOf Bind Var
bind

makeTermEnvs :: CGEnv -> [(GHC.Var, [F.Located F.Expr])] -> [(GHC.Var, GHC.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 {v} {c} {tv} {r}. RTypeV v c tv r -> CoreExpr -> [Var]
collectArgs' [SpecType]
ts [CoreExpr]
ces
    syms :: [[Symbol]]
syms = ([Symbol], [RFInfo], [SpecType], [RReft], SpecType) -> [Symbol]
forall t0 t1 t2 t3 t4. (t0, t1, t2, t3, t4) -> t0
fst5 (([Symbol], [RFInfo], [SpecType], [RReft], SpecType) -> [Symbol])
-> (SpecType
    -> ([Symbol], [RFInfo], [SpecType], [RReft], SpecType))
-> SpecType
-> [Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SpecType -> ([Symbol], [RFInfo], [SpecType], [RReft], SpecType)
forall t t1 a.
RType t t1 a
-> ([Symbol], [RFInfo], [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
    syms' :: [[Symbol]]
syms' = ([Symbol], [RFInfo], [SpecType], [RReft], SpecType) -> [Symbol]
forall t0 t1 t2 t3 t4. (t0, t1, t2, t3, t4) -> t0
fst5 (([Symbol], [RFInfo], [SpecType], [RReft], SpecType) -> [Symbol])
-> (SpecType
    -> ([Symbol], [RFInfo], [SpecType], [RReft], SpecType))
-> SpecType
-> [Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SpecType -> ([Symbol], [RFInfo], [SpecType], [RReft], SpecType)
forall t t1 a.
RType t t1 a
-> ([Symbol], [RFInfo], [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]]
syms [[Symbol]]
syms'
    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]]
syms ((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) (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]
ces)    = [(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
forall v. v -> ExprV v
F.EVar Symbol
y) | (Symbol
x, Symbol
y) <- [Symbol] -> [Symbol] -> [(Symbol, Symbol)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
ys [Symbol]
ys']
    collectArgs' :: RTypeV v c tv r -> CoreExpr -> [Var]
collectArgs' = Int -> CoreExpr -> [Var]
collectArguments (Int -> CoreExpr -> [Var])
-> (RTypeV v c tv r -> Int) -> RTypeV v c tv r -> CoreExpr -> [Var]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Symbol] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([Symbol] -> Int)
-> (RTypeV v c tv r -> [Symbol]) -> RTypeV v c tv r -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTypeRepV v c tv r -> [Symbol]
forall v c tv r. RTypeRepV v c tv r -> [Symbol]
ty_binds (RTypeRepV v c tv r -> [Symbol])
-> (RTypeV v c tv r -> RTypeRepV v c tv r)
-> RTypeV v c tv r
-> [Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTypeV v c tv r -> RTypeRepV v c tv r
forall v c tv r. RTypeV v c tv r -> RTypeRepV v c tv r
toRTypeRep
    err :: a -> String
err a
x        = String
"Constant: makeTermEnvs: no terminating expression for " String -> ShowS
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 (RTypeV Symbol RTyCon RTyVar ()), RReft)]
-> [PVarV Symbol (RTypeV Symbol RTyCon RTyVar ())]
-> [(Symbol, RFInfo, SpecType, RReft)]
-> SpecType
-> SpecType
forall tv v c r.
[(RTVar tv (RTypeV v c tv ()), r)]
-> [PVarV v (RTypeV v c tv ())]
-> [(Symbol, RFInfo, RTypeV v c tv r, r)]
-> RTypeV v c tv r
-> RTypeV v c tv r
mkArrow [(RTVar RTyVar (RTypeV Symbol RTyCon RTyVar ()), RReft)]
αs [PVarV Symbol (RTypeV Symbol RTyCon RTyVar ())]
πs [(Symbol, RFInfo, SpecType, RReft)]
xts (SpecType -> SpecType) -> SpecType -> SpecType
forall a b. (a -> b) -> a -> b
$ [(Symbol, SpecType)] -> RReft -> Oblig -> SpecType -> SpecType
forall v c tv r.
[(Symbol, RTypeV v c tv r)]
-> r -> Oblig -> RTypeV v c tv r -> RTypeV v c tv r
RRTy [] RReft
r Oblig
o SpecType
t2
  where
    ([(RTVar RTyVar (RTypeV Symbol RTyCon RTyVar ()), RReft)]
αs, [PVarV Symbol (RTypeV Symbol RTyCon RTyVar ())]
πs, SpecType
t1) = SpecType
-> ([(RTVar RTyVar (RTypeV Symbol RTyCon RTyVar ()), RReft)],
    [PVarV Symbol (RTypeV Symbol RTyCon RTyVar ())], SpecType)
forall v tv c r.
RTypeV v tv c r
-> ([(RTVar c (RTypeV v tv c ()), r)],
    [PVarV v (RTypeV v tv c ())], RTypeV v tv c r)
bkUniv SpecType
t
    (([Symbol]
xs, [RFInfo]
is, [SpecType]
ts, [RReft]
rs), SpecType
t2) = SpecType -> (([Symbol], [RFInfo], [SpecType], [RReft]), SpecType)
forall v t t1 a.
RTypeV v t t1 a
-> (([Symbol], [RFInfo], [RTypeV v t t1 a], [a]), RTypeV v t t1 a)
bkArrow SpecType
t1
    xts :: [(Symbol, RFInfo, SpecType, RReft)]
xts              = [Symbol]
-> [RFInfo]
-> [SpecType]
-> [RReft]
-> [(Symbol, RFInfo, SpecType, RReft)]
forall t t1 t2 t3. [t] -> [t1] -> [t2] -> [t3] -> [(t, t1, t2, t3)]
zip4 [Symbol]
xs [RFInfo]
is [SpecType]
ts [RReft]
rs

--------------------------------------------------------------------------------
-- | TERMINATION TYPE ----------------------------------------------------------
--------------------------------------------------------------------------------

makeDecrIndex :: (GHC.Var, Template SpecType) -> CG (Maybe Int)
makeDecrIndex :: (Var, Template SpecType) -> CG (Maybe Int)
makeDecrIndex (Var
x, Assumed SpecType
t)
  = do dindex <- Var -> SpecType -> CG (Either (TError SpecType) Int)
forall t. Var -> SpecType -> CG (Either (TError t) Int)
makeDecrIndexTy Var
x SpecType
t
       case dindex of
         Left TError SpecType
msg -> TError SpecType -> CG ()
addWarning TError SpecType
msg CG () -> CG (Maybe Int) -> CG (Maybe Int)
forall a b.
StateT CGInfo Identity a
-> StateT CGInfo Identity b -> StateT CGInfo Identity b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Maybe Int -> CG (Maybe Int)
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Int
forall a. Maybe a
Nothing
         Right Int
i -> Maybe Int -> CG (Maybe Int)
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Int -> CG (Maybe Int)) -> Maybe Int -> CG (Maybe Int)
forall a b. (a -> b) -> a -> b
$ Int -> Maybe Int
forall a. a -> Maybe a
Just Int
i
makeDecrIndex (Var
x, Asserted SpecType
t)
  = do dindex <- Var -> SpecType -> CG (Either (TError SpecType) Int)
forall t. Var -> SpecType -> CG (Either (TError t) Int)
makeDecrIndexTy Var
x SpecType
t
       case dindex of
         Left TError SpecType
msg -> TError SpecType -> CG ()
addWarning TError SpecType
msg CG () -> CG (Maybe Int) -> CG (Maybe Int)
forall a b.
StateT CGInfo Identity a
-> StateT CGInfo Identity b -> StateT CGInfo Identity b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Maybe Int -> CG (Maybe Int)
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Int
forall a. Maybe a
Nothing
         Right Int
i  -> Maybe Int -> CG (Maybe Int)
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Int -> CG (Maybe Int)) -> Maybe Int -> CG (Maybe Int)
forall a b. (a -> b) -> a -> b
$ Int -> Maybe Int
forall a. a -> Maybe a
Just Int
i
makeDecrIndex (Var, Template SpecType)
_ = Maybe Int -> CG (Maybe Int)
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Int
forall a. Maybe a
Nothing

makeDecrIndexTy :: GHC.Var -> SpecType -> CG (Either (TError t) Int)
makeDecrIndexTy :: forall t. Var -> SpecType -> CG (Either (TError t) Int)
makeDecrIndexTy Var
x SpecType
st
  = do autosz <- (CGInfo -> HashSet TyCon) -> StateT CGInfo Identity (HashSet TyCon)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CGInfo -> HashSet TyCon
autoSize
       return $ case dindex autosz of
         Maybe Int
Nothing -> TError t -> Either (TError t) Int
forall a b. a -> Either a b
Left TError t
forall {t}. TError t
msg
         Just Int
i  -> Int -> Either (TError t) Int
forall a b. b -> Either a b
Right Int
i
    where
       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
GHC.getSrcSpan Var
x) [Var -> Doc
forall a. PPrint a => a -> Doc
F.pprint Var
x] (String -> Doc
text String
"No decreasing parameter")
       trep :: RTypeRepV Symbol RTyCon RTyVar RReft
trep = SpecType -> RTypeRepV Symbol RTyCon RTyVar RReft
forall v c tv r. RTypeV v c tv r -> RTypeRepV v c tv r
toRTypeRep (SpecType -> RTypeRepV Symbol RTyCon RTyVar RReft)
-> SpecType -> RTypeRepV Symbol 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
st
       ts :: [SpecType]
ts   = RTypeRepV Symbol RTyCon RTyVar RReft -> [SpecType]
forall v c tv r. RTypeRepV v c tv r -> [RTypeV v c tv r]
ty_args RTypeRepV Symbol RTyCon RTyVar RReft
trep
       cenv :: [RTyVar]
cenv = [SpecType] -> [RTyVar]
forall (t :: * -> *) c b t1.
(Foldable t, TyConable c) =>
t (RType c b t1) -> [b]
makeNumEnv [SpecType]
ts

       p :: HashSet TyCon -> SpecType -> Bool
p HashSet TyCon
autosz SpecType
t = HashSet TyCon -> [RTyVar] -> SpecType -> Bool
isDecreasing HashSet TyCon
autosz [RTyVar]
cenv SpecType
t
       dindex :: HashSet TyCon -> Maybe Int
dindex     HashSet TyCon
autosz = (SpecType -> Bool) -> [SpecType] -> Maybe Int
forall a. (a -> Bool) -> [a] -> Maybe Int
L.findIndex (HashSet TyCon -> SpecType -> Bool
p HashSet TyCon
autosz) [SpecType]
ts

recType :: F.Symbolic a
        => S.HashSet GHC.TyCon
        -> (([a], Maybe Int), (t, Maybe Int, SpecType))
        -> SpecType
recType :: forall a t.
Symbolic a =>
HashSet TyCon
-> (([a], Maybe Int), (t, Maybe Int, SpecType)) -> SpecType
recType HashSet TyCon
_       (([a]
_, Maybe Int
Nothing), (t
_, Maybe Int
Nothing, SpecType
t)) = SpecType
t
recType HashSet TyCon
autoenv (([a]
vs, Maybe Int
indexc), (t
_, Maybe Int
index, SpecType
t))
  = HashSet TyCon
-> SpecType
-> Maybe a
-> Maybe (Symbol, SpecType)
-> Maybe Int
-> SpecType
forall a1 a.
(Enum a1, Eq a1, Num a1, Symbolic a) =>
HashSet TyCon
-> SpecType
-> Maybe a
-> Maybe (Symbol, SpecType)
-> Maybe a1
-> SpecType
makeRecType HashSet TyCon
autoenv SpecType
t Maybe a
v Maybe (Symbol, SpecType)
dxt Maybe Int
index
  where v :: Maybe a
v    = ([a]
vs [a] -> Int -> a
forall a. HasCallStack => [a] -> Int -> a
!!)  (Int -> a) -> Maybe Int -> Maybe a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Int
indexc
        dxt :: Maybe (Symbol, SpecType)
dxt  = ([(Symbol, SpecType)]
xts [(Symbol, SpecType)] -> Int -> (Symbol, SpecType)
forall a. HasCallStack => [a] -> Int -> a
!!) (Int -> (Symbol, SpecType))
-> Maybe Int -> Maybe (Symbol, SpecType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Int
index
        xts :: [(Symbol, SpecType)]
xts  = [Symbol] -> [SpecType] -> [(Symbol, SpecType)]
forall a b. [a] -> [b] -> [(a, b)]
zip (RTypeRepV Symbol RTyCon RTyVar RReft -> [Symbol]
forall v c tv r. RTypeRepV v c tv r -> [Symbol]
ty_binds RTypeRepV Symbol RTyCon RTyVar RReft
trep) (RTypeRepV Symbol RTyCon RTyVar RReft -> [SpecType]
forall v c tv r. RTypeRepV v c tv r -> [RTypeV v c tv r]
ty_args RTypeRepV Symbol RTyCon RTyVar RReft
trep)
        trep :: RTypeRepV Symbol RTyCon RTyVar RReft
trep = SpecType -> RTypeRepV Symbol RTyCon RTyVar RReft
forall v c tv r. RTypeV v c tv r -> RTypeRepV v c tv r
toRTypeRep (SpecType -> RTypeRepV Symbol RTyCon RTyVar RReft)
-> SpecType -> RTypeRepV Symbol 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 :: (GHC.NamedThing t, PPrint t, PPrint a)
           => (t, [a], Template (RType c tv r), Maybe Int)
           -> CG (Maybe (RType c tv r))
checkIndex :: forall t a c tv r.
(NamedThing t, PPrint t, PPrint a) =>
(t, [a], Template (RType c tv r), Maybe Int)
-> CG (Maybe (RType c tv r))
checkIndex (t
_,  [a]
_, Template (RType c tv r)
_, Maybe Int
Nothing   ) = Maybe (RType c tv r)
-> StateT CGInfo Identity (Maybe (RType c tv r))
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (RType c tv r)
forall a. Maybe a
Nothing
checkIndex (t
x, [a]
vs, Template (RType c tv r)
t, Just Int
index) = TError SpecType -> [a] -> Int -> CG (Maybe a)
forall a. TError SpecType -> [a] -> Int -> CG (Maybe a)
safeLogIndex TError SpecType
forall {t}. TError t
msg1 [a]
vs Int
index CG (Maybe a)
-> StateT CGInfo Identity (Maybe (RType c tv r))
-> StateT CGInfo Identity (Maybe (RType c tv r))
forall a b.
StateT CGInfo Identity a
-> StateT CGInfo Identity b -> StateT CGInfo Identity b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> 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
GHC.getSrcSpan t
x
       ts :: [RType c tv r]
ts    = RTypeRepV Symbol c tv r -> [RType c tv r]
forall v c tv r. RTypeRepV v c tv r -> [RTypeV v c tv r]
ty_args (RTypeRepV Symbol c tv r -> [RType c tv r])
-> RTypeRepV Symbol c tv r -> [RType c tv r]
forall a b. (a -> b) -> a -> b
$ RType c tv r -> RTypeRepV Symbol c tv r
forall v c tv r. RTypeV v c tv r -> RTypeRepV v c tv r
toRTypeRep (RType c tv r -> RTypeRepV Symbol c tv r)
-> RType c tv r -> RTypeRepV Symbol 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] (String -> Doc
text String
"No decreasing" Doc -> Doc -> Doc
<+> Int -> Doc
forall a. PPrint a => a -> Doc
F.pprint Int
index Doc -> Doc -> Doc
<-> String -> Doc
text String
"-th argument on" Doc -> Doc -> Doc
<+> Doc
xd Doc -> Doc -> Doc
<+> String -> Doc
text String
"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] (String -> Doc
text  String
"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 GHC.TyCon
            -> SpecType
            -> Maybe a
            -> Maybe (F.Symbol, SpecType)
            -> Maybe a1
            -> SpecType
makeRecType :: forall a1 a.
(Enum a1, Eq a1, Num a1, Symbolic a) =>
HashSet TyCon
-> SpecType
-> Maybe a
-> Maybe (Symbol, SpecType)
-> Maybe a1
-> SpecType
makeRecType HashSet TyCon
autoenv SpecType
t Maybe a
vs Maybe (Symbol, SpecType)
dxs Maybe 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
$ RTypeRepV Symbol RTyCon RTyVar RReft -> SpecType
forall v c tv r. RTypeRepV v c tv r -> RTypeV v c tv r
fromRTypeRep (RTypeRepV Symbol RTyCon RTyVar RReft -> SpecType)
-> RTypeRepV Symbol RTyCon RTyVar RReft -> SpecType
forall a b. (a -> b) -> a -> b
$ RTypeRepV Symbol RTyCon RTyVar RReft
trep {ty_binds = xs', ty_args = 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 (Maybe a1 -> a1
forall a. HasCallStack => Maybe a -> a
fromJust Maybe 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
-> Maybe (a, (Symbol, SpecType))
-> Either (Symbol, SpecType) String
forall a t.
Symbolic a =>
HashSet TyCon
-> Maybe (a, (Symbol, RType RTyCon t RReft))
-> Either (Symbol, RType RTyCon t RReft) String
makeDecrType HashSet TyCon
autoenv Maybe (a, (Symbol, SpecType))
vdxs) [(Symbol, SpecType)]
xts
    vdxs :: Maybe (a, (Symbol, SpecType))
vdxs       = (a -> (Symbol, SpecType) -> (a, (Symbol, SpecType)))
-> Maybe a
-> Maybe (Symbol, SpecType)
-> Maybe (a, (Symbol, SpecType))
forall a b c. (a -> b -> c) -> Maybe a -> Maybe b -> Maybe c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 (,) Maybe a
vs Maybe (Symbol, SpecType)
dxs
    xts :: [(Symbol, SpecType)]
xts        = [Symbol] -> [SpecType] -> [(Symbol, SpecType)]
forall a b. [a] -> [b] -> [(a, b)]
zip (RTypeRepV Symbol RTyCon RTyVar RReft -> [Symbol]
forall v c tv r. RTypeRepV v c tv r -> [Symbol]
ty_binds RTypeRepV Symbol RTyCon RTyVar RReft
trep) (RTypeRepV Symbol RTyCon RTyVar RReft -> [SpecType]
forall v c tv r. RTypeRepV v c tv r -> [RTypeV v c tv r]
ty_args RTypeRepV Symbol RTyCon RTyVar RReft
trep)
    trep :: RTypeRepV Symbol RTyCon RTyVar RReft
trep       = SpecType -> RTypeRepV Symbol RTyCon RTyVar RReft
forall v c tv r. RTypeV v c tv r -> RTypeRepV v c tv r
toRTypeRep (SpecType -> RTypeRepV Symbol RTyCon RTyVar RReft)
-> SpecType -> RTypeRepV Symbol 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 :: forall c tv r. RType c tv r -> RType c tv r
unOCons (RAllT RTVUV Symbol c tv
v RTypeV Symbol c tv r
t r
r)      = RTVUV Symbol c tv
-> RTypeV Symbol c tv r -> r -> RTypeV Symbol c tv r
forall v c tv r.
RTVUV v c tv -> RTypeV v c tv r -> r -> RTypeV v c tv r
RAllT RTVUV Symbol c tv
v (RTypeV Symbol c tv r -> RTypeV Symbol c tv r
forall c tv r. RType c tv r -> RType c tv r
unOCons RTypeV Symbol c tv r
t) r
r
unOCons (RAllP PVUV Symbol c tv
p RTypeV Symbol c tv r
t)        = PVUV Symbol c tv -> RTypeV Symbol c tv r -> RTypeV Symbol c tv r
forall v c tv r. PVUV v c tv -> RTypeV v c tv r -> RTypeV v c tv r
RAllP PVUV Symbol c tv
p (RTypeV Symbol c tv r -> RTypeV Symbol c tv r)
-> RTypeV Symbol c tv r -> RTypeV Symbol c tv r
forall a b. (a -> b) -> a -> b
$ RTypeV Symbol c tv r -> RTypeV Symbol c tv r
forall c tv r. RType c tv r -> RType c tv r
unOCons RTypeV Symbol c tv r
t
unOCons (RFun Symbol
x RFInfo
i RTypeV Symbol c tv r
tx RTypeV Symbol c tv r
t r
r)  = Symbol
-> RFInfo
-> RTypeV Symbol c tv r
-> RTypeV Symbol c tv r
-> r
-> RTypeV Symbol c tv r
forall v c tv r.
Symbol
-> RFInfo
-> RTypeV v c tv r
-> RTypeV v c tv r
-> r
-> RTypeV v c tv r
RFun Symbol
x RFInfo
i (RTypeV Symbol c tv r -> RTypeV Symbol c tv r
forall c tv r. RType c tv r -> RType c tv r
unOCons RTypeV Symbol c tv r
tx) (RTypeV Symbol c tv r -> RTypeV Symbol c tv r
forall c tv r. RType c tv r -> RType c tv r
unOCons RTypeV Symbol c tv r
t) r
r
unOCons (RRTy [(Symbol, RTypeV Symbol c tv r)]
_ r
_ Oblig
OCons RTypeV Symbol c tv r
t) = RTypeV Symbol c tv r -> RTypeV Symbol c tv r
forall c tv r. RType c tv r -> RType c tv r
unOCons RTypeV Symbol c tv r
t
unOCons RTypeV Symbol c tv r
t                  = RTypeV Symbol c tv r
t

mergecondition :: RType c tv r -> RType c tv r -> RType c tv r
mergecondition :: forall c tv r. RType c tv r -> RType c tv r -> RType c tv r
mergecondition (RAllT RTVUV Symbol c tv
_ RTypeV Symbol c tv r
t1 r
_)       (RAllT RTVUV Symbol c tv
v RTypeV Symbol c tv r
t2 r
r2)        = RTVUV Symbol c tv
-> RTypeV Symbol c tv r -> r -> RTypeV Symbol c tv r
forall v c tv r.
RTVUV v c tv -> RTypeV v c tv r -> r -> RTypeV v c tv r
RAllT RTVUV Symbol c tv
v (RTypeV Symbol c tv r
-> RTypeV Symbol c tv r -> RTypeV Symbol c tv r
forall c tv r. RType c tv r -> RType c tv r -> RType c tv r
mergecondition RTypeV Symbol c tv r
t1 RTypeV Symbol c tv r
t2) r
r2
mergecondition (RAllP PVUV Symbol c tv
_ RTypeV Symbol c tv r
t1)         (RAllP PVUV Symbol c tv
p RTypeV Symbol c tv r
t2)           = PVUV Symbol c tv -> RTypeV Symbol c tv r -> RTypeV Symbol c tv r
forall v c tv r. PVUV v c tv -> RTypeV v c tv r -> RTypeV v c tv r
RAllP PVUV Symbol c tv
p (RTypeV Symbol c tv r
-> RTypeV Symbol c tv r -> RTypeV Symbol c tv r
forall c tv r. RType c tv r -> RType c tv r -> RType c tv r
mergecondition RTypeV Symbol c tv r
t1 RTypeV Symbol c tv r
t2)
mergecondition (RRTy [(Symbol, RTypeV Symbol c tv r)]
xts r
r Oblig
OCons RTypeV Symbol c tv r
t1) RTypeV Symbol c tv r
t2                    = [(Symbol, RTypeV Symbol c tv r)]
-> r -> Oblig -> RTypeV Symbol c tv r -> RTypeV Symbol c tv r
forall v c tv r.
[(Symbol, RTypeV v c tv r)]
-> r -> Oblig -> RTypeV v c tv r -> RTypeV v c tv r
RRTy [(Symbol, RTypeV Symbol c tv r)]
xts r
r Oblig
OCons (RTypeV Symbol c tv r
-> RTypeV Symbol c tv r -> RTypeV Symbol c tv r
forall c tv r. RType c tv r -> RType c tv r -> RType c tv r
mergecondition RTypeV Symbol c tv r
t1 RTypeV Symbol c tv r
t2)
mergecondition (RFun Symbol
_ RFInfo
_ RTypeV Symbol c tv r
t11 RTypeV Symbol c tv r
t12 r
_) (RFun Symbol
x2 RFInfo
i RTypeV Symbol c tv r
t21 RTypeV Symbol c tv r
t22 r
r2) = Symbol
-> RFInfo
-> RTypeV Symbol c tv r
-> RTypeV Symbol c tv r
-> r
-> RTypeV Symbol c tv r
forall v c tv r.
Symbol
-> RFInfo
-> RTypeV v c tv r
-> RTypeV v c tv r
-> r
-> RTypeV v c tv r
RFun Symbol
x2 RFInfo
i (RTypeV Symbol c tv r
-> RTypeV Symbol c tv r -> RTypeV Symbol c tv r
forall c tv r. RType c tv r -> RType c tv r -> RType c tv r
mergecondition RTypeV Symbol c tv r
t11 RTypeV Symbol c tv r
t21) (RTypeV Symbol c tv r
-> RTypeV Symbol c tv r -> RTypeV Symbol c tv r
forall c tv r. RType c tv r -> RType c tv r -> RType c tv r
mergecondition RTypeV Symbol c tv r
t12 RTypeV Symbol c tv r
t22) r
r2
mergecondition RTypeV Symbol c tv r
_                     RTypeV Symbol c tv r
t                     = RTypeV Symbol c tv r
t

safeLogIndex :: Error -> [a] -> Int -> CG (Maybe a)
safeLogIndex :: forall a. 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 a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
ls = TError SpecType -> CG ()
addWarning TError SpecType
err CG ()
-> StateT CGInfo Identity (Maybe a)
-> StateT CGInfo Identity (Maybe a)
forall a b.
StateT CGInfo Identity a
-> StateT CGInfo Identity b -> StateT CGInfo Identity b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Maybe a -> StateT CGInfo Identity (Maybe a)
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe a
forall a. Maybe a
Nothing
  | Bool
otherwise      = Maybe a -> StateT CGInfo Identity (Maybe a)
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe a -> StateT CGInfo Identity (Maybe a))
-> Maybe a -> StateT CGInfo Identity (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. HasCallStack => [a] -> Int -> a
!! Int
n

-- RJ: AAAAAAARGHHH!!!!!! THIS CODE IS HORRIBLE!!!!!!!!!
consCBSizedTys :: (Bool -> CGEnv -> (GHC.Var, GHC.CoreExpr, Template SpecType) -> CG (Template SpecType)) ->
                  CGEnv -> [(GHC.Var, GHC.CoreExpr)] -> CG CGEnv
consCBSizedTys :: (Bool
 -> CGEnv
 -> (Var, CoreExpr, Template SpecType)
 -> CG (Template SpecType))
-> CGEnv -> [(Var, CoreExpr)] -> CG CGEnv
consCBSizedTys Bool
-> CGEnv
-> (Var, CoreExpr, Template SpecType)
-> CG (Template SpecType)
consBind CGEnv
γ [(Var, CoreExpr)]
xes
  = do ts'      <- [(Var, CoreExpr)]
-> ((Var, CoreExpr) -> CG (Template SpecType))
-> StateT CGInfo Identity [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) -> CG (Template SpecType))
 -> StateT CGInfo Identity [Template SpecType])
-> ((Var, CoreExpr) -> CG (Template SpecType))
-> StateT CGInfo Identity [Template SpecType]
forall a b. (a -> b) -> a -> b
$ \(Var
x, CoreExpr
e) -> CGEnv -> (Var, Maybe CoreExpr) -> CG (Template SpecType)
varTemplate CGEnv
γ (Var
x, CoreExpr -> Maybe CoreExpr
forall a. a -> Maybe a
Just CoreExpr
e)
       autoenv  <- gets autoSize
       ts       <- forM ts' $ T.mapM refreshArgs
       let 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
       is       <- mapM makeDecrIndex (zip vars ts) >>= checkSameLens
       let xeets = ([Var]
 -> Maybe Int -> [(([Var], Maybe Int), (Var, Maybe Int, SpecType))])
-> [[Var]]
-> [Maybe Int]
-> [[(([Var], Maybe Int), (Var, Maybe Int, SpecType))]]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\[Var]
v Maybe Int
i -> [(([Var]
v,Maybe Int
i), (Var, Maybe Int, SpecType)
x) | (Var, Maybe Int, SpecType)
x <- [Var] -> [Maybe Int] -> [SpecType] -> [(Var, Maybe Int, SpecType)]
forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
zip3 [Var]
vars [Maybe Int]
is ([SpecType] -> [(Var, Maybe Int, SpecType)])
-> [SpecType] -> [(Var, Maybe 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]]
vs [Maybe Int]
is
       _        <- mapM checkIndex (zip4 vars vs ts is) >>= checkEqTypes
       let rts   = (HashSet TyCon
-> (([Var], Maybe Int), (Var, Maybe Int, SpecType)) -> SpecType
forall a t.
Symbolic a =>
HashSet TyCon
-> (([a], Maybe Int), (t, Maybe Int, SpecType)) -> SpecType
recType HashSet TyCon
autoenv ((([Var], Maybe Int), (Var, Maybe Int, SpecType)) -> SpecType)
-> [(([Var], Maybe Int), (Var, Maybe Int, SpecType))] -> [SpecType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) ([(([Var], Maybe Int), (Var, Maybe Int, SpecType))] -> [SpecType])
-> [[(([Var], Maybe Int), (Var, Maybe Int, SpecType))]]
-> [[SpecType]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [[(([Var], Maybe Int), (Var, Maybe Int, SpecType))]]
xeets
       γ'       <- foldM extender γ (zip vars ts)
       let γ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]
vars [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
noMakeRec) ([Var] -> [Var]) -> [[Var]] -> [[Var]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [[Var]]
vs)
       mapM_ (uncurry $ consBind True) (zip γs (zip3 vars es ts))
       return γ'
  where
       noMakeRec :: Var -> Bool
noMakeRec      = if Bool
allowTC then Var -> Bool
GM.isEmbeddedDictVar else Var -> Bool
GM.isPredVar
       allowTC :: Bool
allowTC        = Config -> Bool
typeclass (CGEnv -> Config
forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)
       ([Var]
vars, [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]
vars
       collectArgs' :: Template (RType c tv r) -> CoreExpr -> [Var]
collectArgs'   = Int -> CoreExpr -> [Var]
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 a. [a] -> 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
. RTypeRepV Symbol c tv r -> [Symbol]
forall v c tv r. RTypeRepV v c tv r -> [Symbol]
ty_binds (RTypeRepV Symbol c tv r -> [Symbol])
-> (Template (RType c tv r) -> RTypeRepV Symbol c tv r)
-> Template (RType c tv r)
-> [Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RType c tv r -> RTypeRepV Symbol c tv r
forall v c tv r. RTypeV v c tv r -> RTypeRepV v c tv r
toRTypeRep (RType c tv r -> RTypeRepV Symbol c tv r)
-> (Template (RType c tv r) -> RType c tv r)
-> Template (RType c tv r)
-> RTypeRepV Symbol 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 = TError SpecType
-> (SpecType -> RTypeV Symbol RTyCon RTyVar ())
-> [SpecType]
-> StateT CGInfo Identity [SpecType]
forall b a. Eq b => TError SpecType -> (a -> b) -> [a] -> CG [a]
checkAllVsHead TError SpecType
forall {t}. TError t
err1 SpecType -> RTypeV Symbol RTyCon RTyVar ()
forall v c tv r. RTypeV v c tv r -> RTypeV v c tv ()
toRSort ([Maybe SpecType] -> [SpecType]
forall a. [Maybe a] -> [a]
catMaybes [Maybe SpecType]
x)
       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"
       checkSameLens :: [Maybe Int] -> CG [Maybe Int]
       checkSameLens :: [Maybe Int] -> StateT CGInfo Identity [Maybe Int]
checkSameLens  = TError SpecType
-> (Maybe Int -> Int)
-> [Maybe Int]
-> StateT CGInfo Identity [Maybe Int]
forall b a. Eq b => TError SpecType -> (a -> b) -> [a] -> CG [a]
checkAllVsHead TError SpecType
forall {t}. TError t
err2 Maybe Int -> Int
forall a. Maybe a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length
       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
GHC.getSrcSpan ([Var] -> Var
forall a. HasCallStack => [a] -> a
head [Var]
vars)

       checkAllVsHead :: Eq b => Error -> (a -> b) -> [a] -> CG [a]
       checkAllVsHead :: forall b a. Eq b => TError SpecType -> (a -> b) -> [a] -> CG [a]
checkAllVsHead TError SpecType
_   a -> b
_ []          = [a] -> StateT CGInfo Identity [a]
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return []
       checkAllVsHead 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 a. 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 -> CG ()
addWarning TError SpecType
err CG () -> StateT CGInfo Identity [a] -> StateT CGInfo Identity [a]
forall a b.
StateT CGInfo Identity a
-> StateT CGInfo Identity b -> StateT CGInfo Identity b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [a] -> StateT CGInfo Identity [a]
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return []

-- See Note [Shape of normalized terms] in
-- Language.Haskell.Liquid.Transforms.ANF
collectArguments :: Int -> GHC.CoreExpr -> [GHC.Var]
collectArguments :: Int -> CoreExpr -> [Var]
collectArguments Int
n CoreExpr
e = Int -> [Var] -> [Var]
forall a. Int -> [a] -> [a]
take Int
n ([Var]
vs' [Var] -> [Var] -> [Var]
forall a. [a] -> [a] -> [a]
++ [Var]
vs)
  where
    ([Var]
vs', CoreExpr
e')        = CoreExpr -> ([Var], CoreExpr)
collectValBinders' (CoreExpr -> ([Var], CoreExpr)) -> CoreExpr -> ([Var], CoreExpr)
forall a b. (a -> b) -> a -> b
$ ([Var], CoreExpr) -> CoreExpr
forall a b. (a, b) -> b
snd (([Var], CoreExpr) -> CoreExpr) -> ([Var], CoreExpr) -> CoreExpr
forall a b. (a -> b) -> a -> b
$ CoreExpr -> ([Var], CoreExpr)
GHC.collectTyBinders CoreExpr
e
    vs :: [Var]
vs               = ([Var], CoreExpr) -> [Var]
forall a b. (a, b) -> a
fst (([Var], CoreExpr) -> [Var]) -> ([Var], CoreExpr) -> [Var]
forall a b. (a -> b) -> a -> b
$ CoreExpr -> ([Var], CoreExpr)
forall b. Expr b -> ([b], Expr b)
GHC.collectBinders (CoreExpr -> ([Var], CoreExpr)) -> CoreExpr -> ([Var], CoreExpr)
forall a b. (a -> b) -> a -> b
$ CoreExpr -> CoreExpr
forall b. Expr b -> Expr b
ignoreLetBinds CoreExpr
e'

collectValBinders' :: GHC.CoreExpr -> ([GHC.Var], GHC.CoreExpr)
collectValBinders' :: CoreExpr -> ([Var], CoreExpr)
collectValBinders' = [Var] -> CoreExpr -> ([Var], CoreExpr)
go []
  where
    go :: [Var] -> CoreExpr -> ([Var], CoreExpr)
go [Var]
tvs (GHC.Lam Var
b CoreExpr
e) | Var -> Bool
GHC.isTyVar Var
b = [Var] -> CoreExpr -> ([Var], CoreExpr)
go [Var]
tvs     CoreExpr
e
    go [Var]
tvs (GHC.Lam Var
b CoreExpr
e) | Var -> Bool
GHC.isId    Var
b = [Var] -> CoreExpr -> ([Var], CoreExpr)
go (Var
bVar -> [Var] -> [Var]
forall a. a -> [a] -> [a]
:[Var]
tvs) CoreExpr
e
    go [Var]
tvs (GHC.Tick CoreTickish
_ CoreExpr
e)            = [Var] -> CoreExpr -> ([Var], CoreExpr)
go [Var]
tvs CoreExpr
e
    go [Var]
tvs CoreExpr
e                         = ([Var] -> [Var]
forall a. [a] -> [a]
reverse [Var]
tvs, CoreExpr
e)

ignoreLetBinds :: GHC.Expr b -> GHC.Expr b
ignoreLetBinds :: forall b. Expr b -> Expr b
ignoreLetBinds (GHC.Let (GHC.NonRec b
_ Expr b
_) Expr b
e') = Expr b -> Expr b
forall b. Expr b -> Expr b
ignoreLetBinds Expr b
e'
ignoreLetBinds Expr b
e = Expr b
e

consCBWithExprs :: (Bool -> CGEnv -> (GHC.Var, GHC.CoreExpr, Template SpecType) -> CG (Template SpecType)) ->
                   CGEnv -> [(GHC.Var, GHC.CoreExpr)] -> CG CGEnv
consCBWithExprs :: (Bool
 -> CGEnv
 -> (Var, CoreExpr, Template SpecType)
 -> CG (Template SpecType))
-> CGEnv -> [(Var, CoreExpr)] -> CG CGEnv
consCBWithExprs Bool
-> CGEnv
-> (Var, CoreExpr, Template SpecType)
-> CG (Template SpecType)
consBind CGEnv
γ [(Var, CoreExpr)]
xes
  = do ts0      <- [(Var, CoreExpr)]
-> ((Var, CoreExpr) -> CG (Template SpecType))
-> StateT CGInfo Identity [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) -> CG (Template SpecType))
 -> StateT CGInfo Identity [Template SpecType])
-> ((Var, CoreExpr) -> CG (Template SpecType))
-> StateT CGInfo Identity [Template SpecType]
forall a b. (a -> b) -> a -> b
$ \(Var
x, CoreExpr
e) -> CGEnv -> (Var, Maybe CoreExpr) -> CG (Template SpecType)
varTemplate CGEnv
γ (Var
x, CoreExpr -> Maybe CoreExpr
forall a. a -> Maybe a
Just CoreExpr
e)
       texprs   <- gets termExprs
       let xtes  = (Var -> Maybe (Var, [Located Expr]))
-> [Var] -> [(Var, [Located Expr])]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (Var -> HashMap Var [Located Expr] -> Maybe (Var, [Located Expr])
forall {k} {a}. Hashable k => k -> HashMap k a -> Maybe (k, a)
`lookup'` HashMap Var [Located Expr]
texprs) [Var]
xs
       let ts    = String -> Template SpecType -> SpecType
forall t. String -> Template t -> t
safeFromAsserted String
err (Template SpecType -> SpecType)
-> [Template SpecType] -> [SpecType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Template SpecType]
ts0
       ts'      <- mapM refreshArgs ts
       let 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')
       γ'       <- foldM extender γ xts
       let γs    = CGEnv
-> [(Var, [Located Expr])]
-> [(Var, CoreExpr)]
-> [SpecType]
-> [SpecType]
-> [CGEnv]
makeTermEnvs CGEnv
γ' [(Var, [Located Expr])]
xtes [(Var, CoreExpr)]
xes [SpecType]
ts [SpecType]
ts'
       mapM_ (uncurry $ consBind True) (zip γs (zip3 xs es (Asserted <$> ts')))
       return γ'
  where ([Var]
xs, [CoreExpr]
es) = [(Var, CoreExpr)] -> ([Var], [CoreExpr])
forall a b. [(a, b)] -> ([a], [b])
unzip [(Var, CoreExpr)]
xes
        lookup' :: k -> HashMap k a -> Maybe (k, a)
lookup' k
k HashMap k a
m = (k
k,) (a -> (k, a)) -> Maybe a -> Maybe (k, a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> k -> HashMap k a -> Maybe a
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup k
k HashMap k a
m
        err :: String
err      = String
"Constant: consCBWithExprs"