{-# 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.Applicative (liftA2)
import           Control.Monad.State ( gets, forM, foldM )
import           Text.PrettyPrint.HughesPJ ( (<+>), text )
import           GHC.Types.Var (Var)
import           GHC.Types.Name (NamedThing, getSrcSpan)
import           GHC.Core.TyCon (TyCon)
import           GHC.Core (Bind, CoreExpr, bindersOf)
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)


data TCheck = TerminationCheck | StrataCheck | NoCheck

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 -> Bind Var -> CG Bool
doTermCheck :: Config -> Bind Var -> CG Bool
doTermCheck Config
cfg Bind Var
bind = do
  HashSet Var
lazyVs    <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CGInfo -> HashSet Var
specLazy
  HashSet Var
termVs    <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CGInfo -> HashSet Var
specTmVars
  let skip :: Bool
skip   = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\Var
x -> 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 (forall a. HasConfig a => a -> Bool
structuralTerm Config
cfg) Bool -> Bool -> Bool
|| forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`S.member` HashSet Var
termVs) [Var]
xs
  forall (m :: * -> *) a. Monad m => a -> m a
return     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 forall a. Symbolic a => a -> Bool
GM.isInternal
    xs :: [Var]
xs       = forall b. Bind b -> [b]
bindersOf Bind Var
bind

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

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

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

makeDecrIndex :: (Var, Template SpecType, [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 <- 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 forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
         Right Int
i -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just Int
i
makeDecrIndex (Var
x, Asserted SpecType
t, [Var]
args)
  = do Either (TError SpecType) Int
dindex <- 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 forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
         Right Int
i  -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just Int
i
makeDecrIndex (Var, Template SpecType, [Var])
_ = forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing

makeDecrIndexTy :: Var -> SpecType -> [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 <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CGInfo -> HashSet TyCon
autoSize
       forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ case HashSet TyCon -> Maybe Int
dindex HashSet TyCon
autosz of
         Maybe Int
Nothing -> forall a b. a -> Either a b
Left forall {t}. TError t
msg
         Just Int
i  -> forall a b. b -> Either a b
Right Int
i
    where
       msg :: TError t
msg  = forall t. SrcSpan -> [Doc] -> Doc -> TError t
ErrTermin (forall a. NamedThing a => a -> SrcSpan
getSrcSpan Var
x) [forall a. PPrint a => a -> Doc
F.pprint Var
x] (String -> Doc
text String
"No decreasing parameter")
       trep :: RTypeRep RTyCon RTyVar (UReft Reft)
trep = forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep forall a b. (a -> b) -> a -> b
$ forall c tv r. RType c tv r -> RType c tv r
unOCons SpecType
st
       ts :: [SpecType]
ts   = forall c tv r. RTypeRep c tv r -> [RType c tv r]
ty_args RTypeRep RTyCon RTyVar (UReft Reft)
trep
       tvs :: [(SpecType, Var)]
tvs  = forall a b. [a] -> [b] -> [(a, b)]
zip [SpecType]
ts [Var]
args
       cenv :: [RTyVar]
cenv = 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 = 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 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))
  = 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 forall a. [a] -> Int -> a
!!)  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Int
indexc
        dxt :: Maybe (Symbol, SpecType)
dxt  = ([(Symbol, SpecType)]
xts forall a. [a] -> Int -> a
!!) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Int
index
        xts :: [(Symbol, SpecType)]
xts  = forall a b. [a] -> [b] -> [(a, b)]
zip (forall c tv r. RTypeRep c tv r -> [Symbol]
ty_binds RTypeRep RTyCon RTyVar (UReft Reft)
trep) (forall c tv r. RTypeRep c tv r -> [RType c tv r]
ty_args RTypeRep RTyCon RTyVar (UReft Reft)
trep)
        trep :: RTypeRep RTyCon RTyVar (UReft Reft)
trep = forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep forall a b. (a -> b) -> a -> b
$ forall c tv r. RType c tv r -> RType c tv r
unOCons SpecType
t

checkIndex :: (NamedThing t, PPrint t, PPrint a)
           => (t, [a], Template (RType c tv r), 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   ) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
checkIndex (t
x, [a]
vs, Template (RType c tv r)
t, Just Int
index) = forall a. TError SpecType -> [a] -> Int -> CG (Maybe a)
safeLogIndex forall {t}. TError t
msg1 [a]
vs Int
index forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall a. TError SpecType -> [a] -> Int -> CG (Maybe a)
safeLogIndex forall {t}. TError t
msg2 [RType c tv r]
ts Int
index
    where
       loc :: SrcSpan
loc   = forall a. NamedThing a => a -> SrcSpan
getSrcSpan t
x
       ts :: [RType c tv r]
ts    = forall c tv r. RTypeRep c tv r -> [RType c tv r]
ty_args forall a b. (a -> b) -> a -> b
$ forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep forall a b. (a -> b) -> a -> b
$ forall c tv r. RType c tv r -> RType c tv r
unOCons forall a b. (a -> b) -> a -> b
$ forall t. Template t -> t
unTemplate Template (RType c tv r)
t
       msg1 :: TError t
msg1  = forall t. SrcSpan -> [Doc] -> Doc -> TError t
ErrTermin SrcSpan
loc [Doc
xd] (String -> Doc
text String
"No decreasing" Doc -> Doc -> 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
<+> forall a. PPrint a => a -> Doc
F.pprint [a]
vs)
       msg2 :: TError t
msg2  = forall t. SrcSpan -> [Doc] -> Doc -> TError t
ErrTermin SrcSpan
loc [Doc
xd] (String -> Doc
text  String
"No decreasing parameter")
       xd :: Doc
xd    = forall a. PPrint a => a -> Doc
F.pprint t
x

makeRecType :: (Enum a1, Eq a1, Num a1, F.Symbolic a)
            => S.HashSet 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
  = forall c tv r. RType c tv r -> RType c tv r -> RType c tv r
mergecondition SpecType
t forall a b. (a -> b) -> a -> b
$ forall c tv r. RTypeRep c tv r -> RType c tv r
fromRTypeRep forall a b. (a -> b) -> a -> b
$ RTypeRep RTyCon RTyVar (UReft Reft)
trep {ty_binds :: [Symbol]
ty_binds = [Symbol]
xs', ty_args :: [SpecType]
ty_args = [SpecType]
ts'}
  where
    ([Symbol]
xs', [SpecType]
ts') = forall a b. [(a, b)] -> ([a], [b])
unzip forall a b. (a -> b) -> a -> b
$ forall a t. (Enum a, Eq a, Num a) => a -> t -> [t] -> [t]
replaceN (forall a. HasCallStack => Maybe a -> a
fromJust Maybe a1
is) (forall a b. String -> Either a b -> a
safeFromLeft String
"makeRecType" forall a b. (a -> b) -> a -> b
$ forall a t.
Symbolic a =>
HashSet TyCon
-> Maybe (a, (Symbol, RType RTyCon t (UReft Reft)))
-> Either (Symbol, RType RTyCon t (UReft Reft)) String
makeDecrType HashSet TyCon
autoenv Maybe (a, (Symbol, SpecType))
vdxs) [(Symbol, SpecType)]
xts
    vdxs :: Maybe (a, (Symbol, SpecType))
vdxs       = 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        = forall a b. [a] -> [b] -> [(a, b)]
zip (forall c tv r. RTypeRep c tv r -> [Symbol]
ty_binds RTypeRep RTyCon RTyVar (UReft Reft)
trep) (forall c tv r. RTypeRep c tv r -> [RType c tv r]
ty_args RTypeRep RTyCon RTyVar (UReft Reft)
trep)
    trep :: RTypeRep RTyCon RTyVar (UReft Reft)
trep       = forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep forall a b. (a -> b) -> a -> b
$ 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)      = forall c tv r. RTVU c tv -> RType c tv r -> r -> RType c tv r
RAllT RTVU c tv
v (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)        = forall c tv r. PVU c tv -> RType c tv r -> RType c tv r
RAllP PVU c tv
p forall a b. (a -> b) -> a -> b
$ 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)  = forall c tv r.
Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
x RFInfo
i (forall c tv r. RType c tv r -> RType c tv r
unOCons RType c tv r
tx) (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) = 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)        = forall c tv r. RTVU c tv -> RType c tv r -> r -> RType c tv r
RAllT RTVU c tv
v (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)           = forall c tv r. PVU c tv -> RType c tv r -> RType c tv r
RAllP PVU c tv
p (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                    = 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 (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) = forall c tv r.
Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
x2 RFInfo
i (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) (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 forall a. Ord a => a -> a -> Bool
>= forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
ls = TError SpecType -> CG ()
addWarning TError SpecType
err forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
  | Bool
otherwise      = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ [a]
ls forall a. [a] -> Int -> a
!! Int
n

-- RJ: AAAAAAARGHHH!!!!!! THIS CODE IS HORRIBLE!!!!!!!!!
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))
-> CGEnv -> [(Var, CoreExpr)] -> CG CGEnv
consCBSizedTys Bool
-> CGEnv
-> (Var, CoreExpr, Template SpecType)
-> CG (Template SpecType)
consBind CGEnv
γ [(Var, CoreExpr)]
xes
  = do [Template SpecType]
ts'      <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Var, CoreExpr)]
xes forall a b. (a -> b) -> a -> b
$ \(Var
x, CoreExpr
e) -> CGEnv -> (Var, Maybe CoreExpr) -> CG (Template SpecType)
varTemplate CGEnv
γ (Var
x, forall a. a -> Maybe a
Just CoreExpr
e)
       HashSet TyCon
autoenv  <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CGInfo -> HashSet TyCon
autoSize
       [Template SpecType]
ts       <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Template SpecType]
ts' forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
T.mapM forall (m :: * -> *). FreshM m => SpecType -> m SpecType
refreshArgs
       let vs :: [[Var]]
vs    = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall {c} {tv} {r}. Template (RType c tv r) -> CoreExpr -> [Var]
collectArgs' [Template SpecType]
ts [CoreExpr]
es
       [Maybe Int]
is       <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Var, Template SpecType, [Var]) -> CG (Maybe Int)
makeDecrIndex (forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
zip3 [Var]
vars [Template SpecType]
ts [[Var]]
vs) 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 = 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 <- forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
zip3 [Var]
vars [Maybe Int]
is forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall t. Template t -> t
unTemplate [Template SpecType]
ts]) [[Var]]
vs [Maybe Int]
is
       [SpecType]
_        <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM 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 (forall t t1 t2 t3. [t] -> [t1] -> [t2] -> [t3] -> [(t, t1, t2, t3)]
zip4 [Var]
vars [[Var]]
vs [Template SpecType]
ts [Maybe Int]
is) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [Maybe SpecType] -> StateT CGInfo Identity [SpecType]
checkEqTypes
       let rts :: [[SpecType]]
rts   = (forall a t.
Symbolic a =>
HashSet TyCon
-> (([a], Maybe Int), (t, Maybe Int, SpecType)) -> SpecType
recType HashSet TyCon
autoenv forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [[(([Var], Maybe Int), (Var, Maybe Int, SpecType))]]
xeets
       CGEnv
γ'       <- forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM forall a. Symbolic a => CGEnv -> (a, Template SpecType) -> CG CGEnv
extender CGEnv
γ (forall a b. [a] -> [b] -> [(a, b)]
zip [Var]
vars [Template SpecType]
ts)
       let γs :: [CGEnv]
γs    = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith CGEnv -> [Var] -> CGEnv
makeRecInvariants [CGEnv
γ' CGEnv -> [(Var, SpecType)] -> CGEnv
`setTRec` forall a b. [a] -> [b] -> [(a, b)]
zip [Var]
vars [SpecType]
rts' | [SpecType]
rts' <- [[SpecType]]
rts] (forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> Bool
noMakeRec) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [[Var]]
vs)
       forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a b. (a -> b) -> a -> b
$ Bool
-> CGEnv
-> (Var, CoreExpr, Template SpecType)
-> CG (Template SpecType)
consBind Bool
True) (forall a b. [a] -> [b] -> [(a, b)]
zip [CGEnv]
γs (forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
zip3 [Var]
vars [CoreExpr]
es [Template SpecType]
ts))
       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 (forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)
       ([Var]
vars, [CoreExpr]
es)     = forall a b. [(a, b)] -> ([a], [b])
unzip [(Var, CoreExpr)]
xes
       dxs :: [Doc]
dxs            = forall a. PPrint a => a -> Doc
F.pprint 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]
GM.collectArguments forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t a -> Int
length forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall c tv r. RTypeRep c tv r -> [Symbol]
ty_binds forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall c tv r. RType c tv r -> RType c tv r
unOCons forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. Template t -> t
unTemplate
       checkEqTypes :: [Maybe SpecType] -> CG [SpecType]
       checkEqTypes :: [Maybe SpecType] -> StateT CGInfo Identity [SpecType]
checkEqTypes [Maybe SpecType]
x = forall b a. Eq b => TError SpecType -> (a -> b) -> [a] -> CG [a]
checkAllVsHead forall {t}. TError t
err1 forall c tv r. RType c tv r -> RType c tv ()
toRSort (forall a. [Maybe a] -> [a]
catMaybes [Maybe SpecType]
x)
       err1 :: TError t
err1           = forall t. SrcSpan -> [Doc] -> Doc -> TError t
ErrTermin SrcSpan
loc [Doc]
dxs 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  = forall b a. Eq b => TError SpecType -> (a -> b) -> [a] -> CG [a]
checkAllVsHead forall {t}. TError t
err2 forall (t :: * -> *) a. Foldable t => t a -> Int
length
       err2 :: TError t
err2           = forall t. SrcSpan -> [Doc] -> Doc -> TError t
ErrTermin SrcSpan
loc [Doc]
dxs 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            = forall a. NamedThing a => a -> SrcSpan
getSrcSpan (forall a. [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
_ []          = forall (m :: * -> *) a. Monad m => a -> m a
return []
       checkAllVsHead TError SpecType
err a -> b
f (a
x:[a]
xs)
         | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall a. Eq a => a -> a -> Bool
== a -> b
f a
x) (a -> b
f forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a]
xs) = forall (m :: * -> *) a. Monad m => a -> m a
return (a
xforall a. a -> [a] -> [a]
:[a]
xs)
         | Bool
otherwise               = TError SpecType -> CG ()
addWarning TError SpecType
err forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return []

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