{-# LANGUAGE TupleSections #-}
-- | 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.Fixpoint.Types.PrettyPrint (PPrint)
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.Transforms.Rec (isIdTRecBound)
import           Language.Haskell.Liquid.Types (refreshArgs, HasConfig (..), toRSort)
import           Language.Haskell.Liquid.Types.Types
  (SpecType, TError (..), RType (..), RTypeRep (..), Oblig (..), Error, Config (..), RReft,
   toRTypeRep, structuralTerm, bkArrowDeep, mkArrow, bkUniv, bkArrow, fromRTypeRep)
import           Language.Haskell.Liquid.Types.RefType (isDecreasing, makeDecrType, makeLexRefa, makeNumEnv)
import           Language.Haskell.Liquid.Misc (safeFromLeft, replaceN, (<->), zip4, safeFromJust, fst5)
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
  HashSet Var
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
  HashSet Var
termVs    <- (CGInfo -> HashSet Var) -> StateT CGInfo Identity (HashSet Var)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CGInfo -> HashSet Var
specTmVars
  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
nocheck 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 -> HashSet Var -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`S.member` HashSet Var
termVs) [Var]
xs
  Bool -> CG Bool
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return     (Bool -> CG Bool) -> Bool -> CG Bool
forall a b. (a -> b) -> a -> b
$ Bool
chk Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
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 {c} {tv} {r}. RType 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
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]
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 a. [a] -> 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 -> 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 (RType RTyCon RTyVar ()), RReft)]
-> [PVar (RType RTyCon RTyVar ())]
-> [(Symbol, RFInfo, SpecType, RReft)]
-> SpecType
-> SpecType
forall tv c r.
[(RTVar tv (RType c tv ()), r)]
-> [PVar (RType c tv ())]
-> [(Symbol, RFInfo, 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, RFInfo, 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, [RFInfo]
is, [SpecType]
ts, [RReft]
rs), SpecType
t2) = 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)
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, [GHC.Var]) -> CG (Maybe Int)
makeDecrIndex :: (Var, Template SpecType, [Var]) -> CG (Maybe Int)
makeDecrIndex (Var
x, Assumed 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 -> 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, [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 -> 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, [Var])
_ = 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 -> [GHC.Var] -> CG (Either (TError t) Int)
makeDecrIndexTy :: forall t. Var -> SpecType -> [Var] -> CG (Either (TError t) Int)
makeDecrIndexTy Var
x SpecType
st [Var]
args
  = do HashSet TyCon
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
       Either (TError t) Int -> CG (Either (TError t) Int)
forall a. a -> StateT CGInfo Identity a
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
$ case HashSet TyCon -> Maybe Int
dindex HashSet TyCon
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 :: 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
st
       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
       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, 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)
       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

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 (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 :: (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    = 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] (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
$ 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 = 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 (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 :: forall c tv r. 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 RFInfo
i RType c tv r
tx RType c tv r
t r
r)  = Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
forall c tv r.
Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
x RFInfo
i (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 :: forall c tv r. 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
_ RFInfo
_ RType c tv r
t11 RType c tv r
t12 r
_) (RFun Symbol
x2 RFInfo
i RType c tv r
t21 RType c tv r
t22 r
r2) = Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
forall c tv r.
Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
x2 RFInfo
i (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 :: 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 [Template SpecType]
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)
       HashSet TyCon
autoenv  <- (CGInfo -> HashSet TyCon) -> StateT CGInfo Identity (HashSet TyCon)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CGInfo -> HashSet TyCon
autoSize
       [Template SpecType]
ts       <- [Template SpecType]
-> (Template SpecType -> 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 [Template SpecType]
ts' ((Template SpecType -> CG (Template SpecType))
 -> StateT CGInfo Identity [Template SpecType])
-> (Template SpecType -> CG (Template SpecType))
-> StateT CGInfo Identity [Template SpecType]
forall a b. (a -> b) -> a -> b
$ (SpecType -> StateT CGInfo Identity SpecType)
-> Template SpecType -> CG (Template SpecType)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Template a -> m (Template b)
T.mapM SpecType -> StateT CGInfo Identity SpecType
forall (m :: * -> *). FreshM m => SpecType -> m SpecType
refreshArgs
       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
       [Maybe Int]
is       <- ((Var, Template SpecType, [Var]) -> CG (Maybe Int))
-> [(Var, Template SpecType, [Var])]
-> StateT CGInfo Identity [Maybe Int]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Var, Template SpecType, [Var]) -> CG (Maybe Int)
makeDecrIndex ([Var]
-> [Template SpecType]
-> [[Var]]
-> [(Var, Template SpecType, [Var])]
forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
zip3 [Var]
vars [Template SpecType]
ts [[Var]]
vs) StateT CGInfo Identity [Maybe Int]
-> ([Maybe Int] -> StateT CGInfo Identity [Maybe Int])
-> StateT CGInfo Identity [Maybe Int]
forall a b.
StateT CGInfo Identity a
-> (a -> StateT CGInfo Identity b) -> StateT CGInfo Identity b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [Maybe Int] -> StateT CGInfo Identity [Maybe Int]
checkSameLens
       let xeets :: [[(([Var], Maybe Int), (Var, Maybe Int, SpecType))]]
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
       [SpecType]
_        <- ((Var, [Var], Template SpecType, Maybe Int)
 -> StateT CGInfo Identity (Maybe SpecType))
-> [(Var, [Var], Template SpecType, Maybe Int)]
-> StateT CGInfo Identity [Maybe SpecType]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Var, [Var], Template SpecType, Maybe 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), Maybe Int)
-> CG (Maybe (RType c tv r))
checkIndex ([Var]
-> [[Var]]
-> [Template SpecType]
-> [Maybe Int]
-> [(Var, [Var], Template SpecType, Maybe Int)]
forall t t1 t2 t3. [t] -> [t1] -> [t2] -> [t3] -> [(t, t1, t2, t3)]
zip4 [Var]
vars [[Var]]
vs [Template SpecType]
ts [Maybe Int]
is) StateT CGInfo Identity [Maybe SpecType]
-> ([Maybe SpecType] -> StateT CGInfo Identity [SpecType])
-> StateT CGInfo Identity [SpecType]
forall a b.
StateT CGInfo Identity a
-> (a -> StateT CGInfo Identity b) -> StateT CGInfo Identity b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [Maybe SpecType] -> StateT CGInfo Identity [SpecType]
checkEqTypes
       let rts :: [[SpecType]]
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
       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] -> [(Var, Template SpecType)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Var]
vars [Template SpecType]
ts)
       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]
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)
       ((CGEnv, (Var, CoreExpr, Template SpecType))
 -> CG (Template SpecType))
-> [(CGEnv, (Var, CoreExpr, Template SpecType))] -> CG ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((CGEnv
 -> (Var, CoreExpr, Template SpecType) -> CG (Template SpecType))
-> (CGEnv, (Var, CoreExpr, Template SpecType))
-> CG (Template SpecType)
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((CGEnv
  -> (Var, CoreExpr, Template SpecType) -> CG (Template SpecType))
 -> (CGEnv, (Var, CoreExpr, Template SpecType))
 -> CG (Template SpecType))
-> (CGEnv
    -> (Var, CoreExpr, Template SpecType) -> CG (Template SpecType))
-> (CGEnv, (Var, CoreExpr, Template SpecType))
-> CG (Template SpecType)
forall a b. (a -> b) -> a -> b
$ Bool
-> CGEnv
-> (Var, CoreExpr, Template SpecType)
-> CG (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]
-> [(Var, CoreExpr, Template SpecType)]
forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
zip3 [Var]
vars [CoreExpr]
es [Template SpecType]
ts))
       CGEnv -> CG CGEnv
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return CGEnv
γ'
  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
. 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 = TError SpecType
-> (SpecType -> RType 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 -> 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]
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 [Template SpecType]
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)
       HashMap Var [Located Expr]
texprs   <- (CGInfo -> HashMap Var [Located Expr])
-> StateT CGInfo Identity (HashMap Var [Located Expr])
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CGInfo -> HashMap Var [Located Expr]
termExprs
       let xtes :: [(Var, [Located Expr])]
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 :: [SpecType]
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
       [SpecType]
ts'      <- (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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM SpecType -> StateT CGInfo Identity 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'
       ((CGEnv, (Var, CoreExpr, Template SpecType))
 -> CG (Template SpecType))
-> [(CGEnv, (Var, CoreExpr, Template SpecType))] -> CG ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((CGEnv
 -> (Var, CoreExpr, Template SpecType) -> CG (Template SpecType))
-> (CGEnv, (Var, CoreExpr, Template SpecType))
-> CG (Template SpecType)
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((CGEnv
  -> (Var, CoreExpr, Template SpecType) -> CG (Template SpecType))
 -> (CGEnv, (Var, CoreExpr, Template SpecType))
 -> CG (Template SpecType))
-> (CGEnv
    -> (Var, CoreExpr, Template SpecType) -> CG (Template SpecType))
-> (CGEnv, (Var, CoreExpr, Template SpecType))
-> CG (Template SpecType)
forall a b. (a -> b) -> a -> b
$ Bool
-> CGEnv
-> (Var, CoreExpr, Template SpecType)
-> CG (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]
-> [(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 -> CG CGEnv
forall a. a -> StateT CGInfo Identity a
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' :: 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"