{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings     #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TupleSections         #-}
{-# LANGUAGE UndecidableInstances  #-}
{-# LANGUAGE ConstraintKinds       #-}

module Language.Haskell.Liquid.Types.Fresh
  ( Freshable(..)
  , refreshTy
  , refreshVV
  , refreshArgs
  , refreshHoles
  , refreshArgsSub
  )
  where

import           Data.Maybe                    (catMaybes) -- , fromJust, isJust)
import           Data.Bifunctor
import qualified Data.List                      as L
-- import qualified Data.HashMap.Strict            as M
-- import qualified Data.HashSet                   as S
-- import           Data.Hashable
-- import           Control.Monad.State            (gets, get, put, modify)
-- import           Control.Monad                  (when, (>=>))
-- import           CoreUtils  (exprType)
import           Prelude                        hiding (error)
-- import           Type       (Type)
-- import           CoreSyn
-- import           Var        (varType, isTyVar, Var)

import qualified Language.Fixpoint.Types as F
-- import           Language.Fixpoint.Types.Visitor (kvars)
import           Language.Haskell.Liquid.Misc  (single)
import           Language.Haskell.Liquid.Types.Types
import           Language.Haskell.Liquid.Types.RefType


class (Applicative m, Monad m) => Freshable m a where
  fresh   :: m a
  true    :: Bool -> a -> m a
  true Bool
_  = a -> m a
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return
  refresh :: Bool -> a -> m a
  refresh Bool
_ = a -> m a
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return


instance (Freshable m Integer, Monad m, Applicative m) => Freshable m F.Symbol where
  fresh :: m Symbol
fresh = Symbol -> Integer -> Symbol
F.tempSymbol Symbol
"x" (Integer -> Symbol) -> m Integer -> m Symbol
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Integer
forall (m :: * -> *) a. Freshable m a => m a
fresh

instance (Freshable m Integer, Monad m, Applicative m) => Freshable m F.Expr where
  fresh :: m Expr
fresh  = Integer -> Expr
kv (Integer -> Expr) -> m Integer -> m Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Integer
forall (m :: * -> *) a. Freshable m a => m a
fresh
    where
      kv :: Integer -> Expr
kv = (KVar -> Subst -> Expr
`F.PKVar` Subst
forall a. Monoid a => a
mempty) (KVar -> Expr) -> (Integer -> KVar) -> Integer -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> KVar
F.intKvar

instance (Freshable m Integer, Monad m, Applicative m) => Freshable m [F.Expr] where
  fresh :: m [Expr]
fresh = Expr -> [Expr]
forall t. t -> [t]
single (Expr -> [Expr]) -> m Expr -> m [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Expr
forall (m :: * -> *) a. Freshable m a => m a
fresh

instance (Freshable m Integer, Monad m, Applicative m) => Freshable m F.Reft where
  fresh :: m Reft
fresh                  = Maybe SrcSpan -> String -> m Reft
forall a. Maybe SrcSpan -> String -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing String
"fresh Reft"
  true :: Bool -> Reft -> m Reft
true    Bool
_ (F.Reft (Symbol
v,Expr
_)) = Reft -> m Reft
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Reft -> m Reft) -> Reft -> m Reft
forall a b. (a -> b) -> a -> b
$ (Symbol, Expr) -> Reft
F.Reft (Symbol
v, Expr
forall a. Monoid a => a
mempty)
  refresh :: Bool -> Reft -> m Reft
refresh Bool
_ (F.Reft (Symbol
_,Expr
_)) = ((Symbol, Expr) -> Reft
F.Reft ((Symbol, Expr) -> Reft)
-> (Expr -> (Symbol, Expr)) -> Expr -> Reft
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) ((Expr -> (Symbol, Expr)) -> Expr -> Reft)
-> (Symbol -> Expr -> (Symbol, Expr)) -> Symbol -> Expr -> Reft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (,) (Symbol -> Expr -> Reft) -> m Symbol -> m (Expr -> Reft)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Symbol
freshVV m (Expr -> Reft) -> m Expr -> m Reft
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> m Expr
forall (m :: * -> *) a. Freshable m a => m a
fresh
    where
      freshVV :: m Symbol
freshVV            = Maybe Integer -> Symbol
F.vv (Maybe Integer -> Symbol)
-> (Integer -> Maybe Integer) -> Integer -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Maybe Integer
forall a. a -> Maybe a
Just (Integer -> Symbol) -> m Integer -> m Symbol
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Integer
forall (m :: * -> *) a. Freshable m a => m a
fresh

instance Freshable m Integer => Freshable m RReft where
  fresh :: m RReft
fresh             = Maybe SrcSpan -> String -> m RReft
forall a. Maybe SrcSpan -> String -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing String
"fresh RReft"
  true :: Bool -> RReft -> m RReft
true Bool
allowTC (MkUReft Reft
r Predicate
_)    = Reft -> Predicate -> RReft
forall r. r -> Predicate -> UReft r
MkUReft (Reft -> Predicate -> RReft) -> m Reft -> m (Predicate -> RReft)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> Reft -> m Reft
forall (m :: * -> *) a. Freshable m a => Bool -> a -> m a
true Bool
allowTC Reft
r    m (Predicate -> RReft) -> m Predicate -> m RReft
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Predicate -> m Predicate
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Predicate
forall a. Monoid a => a
mempty
  refresh :: Bool -> RReft -> m RReft
refresh Bool
allowTC (MkUReft Reft
r Predicate
_) = Reft -> Predicate -> RReft
forall r. r -> Predicate -> UReft r
MkUReft (Reft -> Predicate -> RReft) -> m Reft -> m (Predicate -> RReft)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> Reft -> m Reft
forall (m :: * -> *) a. Freshable m a => Bool -> a -> m a
refresh Bool
allowTC Reft
r m (Predicate -> RReft) -> m Predicate -> m RReft
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Predicate -> m Predicate
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Predicate
forall a. Monoid a => a
mempty

instance (Freshable m Integer, Freshable m r, F.Reftable r ) => Freshable m (RRType r) where
  fresh :: m (RRType r)
fresh   = Maybe SrcSpan -> String -> m (RRType r)
forall a. Maybe SrcSpan -> String -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing String
"fresh RefType"
  refresh :: Bool -> RRType r -> m (RRType r)
refresh = Bool -> RRType r -> m (RRType r)
forall (m :: * -> *) r.
(Freshable m Integer, Freshable m r, Reftable r) =>
Bool -> RRType r -> m (RRType r)
refreshRefType
  true :: Bool -> RRType r -> m (RRType r)
true    = Bool -> RRType r -> m (RRType r)
forall (m :: * -> *) r.
(Freshable m Integer, Freshable m r, Reftable r) =>
Bool -> RRType r -> m (RRType r)
trueRefType

-----------------------------------------------------------------------------------------------
trueRefType :: (Freshable m Integer, Freshable m r, F.Reftable r) => Bool -> RRType r -> m (RRType r)
-----------------------------------------------------------------------------------------------
trueRefType :: forall (m :: * -> *) r.
(Freshable m Integer, Freshable m r, Reftable r) =>
Bool -> RRType r -> m (RRType r)
trueRefType Bool
allowTC (RAllT RTVU RTyCon RTyVar
α RType RTyCon RTyVar r
t r
r)
  = RTVU RTyCon RTyVar
-> RType RTyCon RTyVar r -> r -> RType RTyCon RTyVar r
forall c tv r. RTVU c tv -> RType c tv r -> r -> RType c tv r
RAllT RTVU RTyCon RTyVar
α (RType RTyCon RTyVar r -> r -> RType RTyCon RTyVar r)
-> m (RType RTyCon RTyVar r) -> m (r -> RType RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> RType RTyCon RTyVar r -> m (RType RTyCon RTyVar r)
forall (m :: * -> *) a. Freshable m a => Bool -> a -> m a
true Bool
allowTC RType RTyCon RTyVar r
t m (r -> RType RTyCon RTyVar r) -> m r -> m (RType RTyCon RTyVar r)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Bool -> r -> m r
forall (m :: * -> *) a. Freshable m a => Bool -> a -> m a
true Bool
allowTC r
r

trueRefType Bool
allowTC (RAllP PVU RTyCon RTyVar
π RType RTyCon RTyVar r
t)
  = PVU RTyCon RTyVar -> RType RTyCon RTyVar r -> RType RTyCon RTyVar r
forall c tv r. PVU c tv -> RType c tv r -> RType c tv r
RAllP PVU RTyCon RTyVar
π (RType RTyCon RTyVar r -> RType RTyCon RTyVar r)
-> m (RType RTyCon RTyVar r) -> m (RType RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> RType RTyCon RTyVar r -> m (RType RTyCon RTyVar r)
forall (m :: * -> *) a. Freshable m a => Bool -> a -> m a
true Bool
allowTC RType RTyCon RTyVar r
t

trueRefType Bool
allowTC (RFun Symbol
_ RFInfo
_ RType RTyCon RTyVar r
t RType RTyCon RTyVar r
t' r
_)
  -- YL: attaching rfinfo here is crucial
  = RFInfo
-> Symbol
-> RType RTyCon RTyVar r
-> RType RTyCon RTyVar r
-> RType RTyCon RTyVar r
forall r c tv.
Monoid r =>
RFInfo -> Symbol -> RType c tv r -> RType c tv r -> RType c tv r
rFun' (Bool -> RFInfo
classRFInfo Bool
allowTC) (Symbol
 -> RType RTyCon RTyVar r
 -> RType RTyCon RTyVar r
 -> RType RTyCon RTyVar r)
-> m Symbol
-> m (RType RTyCon RTyVar r
      -> RType RTyCon RTyVar r -> RType RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Symbol
forall (m :: * -> *) a. Freshable m a => m a
fresh m (RType RTyCon RTyVar r
   -> RType RTyCon RTyVar r -> RType RTyCon RTyVar r)
-> m (RType RTyCon RTyVar r)
-> m (RType RTyCon RTyVar r -> RType RTyCon RTyVar r)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Bool -> RType RTyCon RTyVar r -> m (RType RTyCon RTyVar r)
forall (m :: * -> *) a. Freshable m a => Bool -> a -> m a
true Bool
allowTC RType RTyCon RTyVar r
t m (RType RTyCon RTyVar r -> RType RTyCon RTyVar r)
-> m (RType RTyCon RTyVar r) -> m (RType RTyCon RTyVar r)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Bool -> RType RTyCon RTyVar r -> m (RType RTyCon RTyVar r)
forall (m :: * -> *) a. Freshable m a => Bool -> a -> m a
true Bool
allowTC RType RTyCon RTyVar r
t'

trueRefType Bool
allowTC (RApp RTyCon
c [RType RTyCon RTyVar r]
ts [RTProp RTyCon RTyVar r]
_  r
_) | if Bool
allowTC then RTyCon -> Bool
forall c. TyConable c => c -> Bool
isEmbeddedDict RTyCon
c else RTyCon -> Bool
forall c. TyConable c => c -> Bool
isClass RTyCon
c
  = RTyCon -> [RType RTyCon RTyVar r] -> RType RTyCon RTyVar r
forall r c tv. Monoid r => c -> [RType c tv r] -> RType c tv r
rRCls RTyCon
c ([RType RTyCon RTyVar r] -> RType RTyCon RTyVar r)
-> m [RType RTyCon RTyVar r] -> m (RType RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (RType RTyCon RTyVar r -> m (RType RTyCon RTyVar r))
-> [RType RTyCon RTyVar r] -> m [RType RTyCon RTyVar r]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Bool -> RType RTyCon RTyVar r -> m (RType RTyCon RTyVar r)
forall (m :: * -> *) a. Freshable m a => Bool -> a -> m a
true Bool
allowTC) [RType RTyCon RTyVar r]
ts

trueRefType Bool
allowTC (RApp RTyCon
c [RType RTyCon RTyVar r]
ts [RTProp RTyCon RTyVar r]
rs r
r)
  = RTyCon
-> [RType RTyCon RTyVar r]
-> [RTProp RTyCon RTyVar r]
-> r
-> RType RTyCon RTyVar r
forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp RTyCon
c ([RType RTyCon RTyVar r]
 -> [RTProp RTyCon RTyVar r] -> r -> RType RTyCon RTyVar r)
-> m [RType RTyCon RTyVar r]
-> m ([RTProp RTyCon RTyVar r] -> r -> RType RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (RType RTyCon RTyVar r -> m (RType RTyCon RTyVar r))
-> [RType RTyCon RTyVar r] -> m [RType RTyCon RTyVar r]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Bool -> RType RTyCon RTyVar r -> m (RType RTyCon RTyVar r)
forall (m :: * -> *) a. Freshable m a => Bool -> a -> m a
true Bool
allowTC) [RType RTyCon RTyVar r]
ts m ([RTProp RTyCon RTyVar r] -> r -> RType RTyCon RTyVar r)
-> m [RTProp RTyCon RTyVar r] -> m (r -> RType RTyCon RTyVar r)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (RTProp RTyCon RTyVar r -> m (RTProp RTyCon RTyVar r))
-> [RTProp RTyCon RTyVar r] -> m [RTProp RTyCon RTyVar r]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Bool -> RTProp RTyCon RTyVar r -> m (RTProp RTyCon RTyVar r)
forall r (f :: * -> *) τ.
(Reftable r, Freshable f r, Freshable f Integer) =>
Bool
-> Ref τ (RType RTyCon RTyVar r)
-> f (Ref τ (RType RTyCon RTyVar r))
trueRef Bool
allowTC) [RTProp RTyCon RTyVar r]
rs m (r -> RType RTyCon RTyVar r) -> m r -> m (RType RTyCon RTyVar r)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Bool -> r -> m r
forall (m :: * -> *) a. Freshable m a => Bool -> a -> m a
true Bool
allowTC r
r

trueRefType Bool
allowTC (RAppTy RType RTyCon RTyVar r
t RType RTyCon RTyVar r
t' r
_)
  = RType RTyCon RTyVar r
-> RType RTyCon RTyVar r -> r -> RType RTyCon RTyVar r
forall c tv r. RType c tv r -> RType c tv r -> r -> RType c tv r
RAppTy (RType RTyCon RTyVar r
 -> RType RTyCon RTyVar r -> r -> RType RTyCon RTyVar r)
-> m (RType RTyCon RTyVar r)
-> m (RType RTyCon RTyVar r -> r -> RType RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> RType RTyCon RTyVar r -> m (RType RTyCon RTyVar r)
forall (m :: * -> *) a. Freshable m a => Bool -> a -> m a
true Bool
allowTC RType RTyCon RTyVar r
t m (RType RTyCon RTyVar r -> r -> RType RTyCon RTyVar r)
-> m (RType RTyCon RTyVar r) -> m (r -> RType RTyCon RTyVar r)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Bool -> RType RTyCon RTyVar r -> m (RType RTyCon RTyVar r)
forall (m :: * -> *) a. Freshable m a => Bool -> a -> m a
true Bool
allowTC RType RTyCon RTyVar r
t' m (r -> RType RTyCon RTyVar r) -> m r -> m (RType RTyCon RTyVar r)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> r -> m r
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return r
forall a. Monoid a => a
mempty

trueRefType Bool
allowTC (RVar RTyVar
a r
r)
  = RTyVar -> r -> RType RTyCon RTyVar r
forall c tv r. tv -> r -> RType c tv r
RVar RTyVar
a (r -> RType RTyCon RTyVar r) -> m r -> m (RType RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> r -> m r
forall (m :: * -> *) a. Freshable m a => Bool -> a -> m a
true Bool
allowTC r
r

trueRefType Bool
allowTC (RAllE Symbol
y RType RTyCon RTyVar r
ty RType RTyCon RTyVar r
tx)
  = do Symbol
y'  <- m Symbol
forall (m :: * -> *) a. Freshable m a => m a
fresh
       RType RTyCon RTyVar r
ty' <- Bool -> RType RTyCon RTyVar r -> m (RType RTyCon RTyVar r)
forall (m :: * -> *) a. Freshable m a => Bool -> a -> m a
true Bool
allowTC RType RTyCon RTyVar r
ty
       RType RTyCon RTyVar r
tx' <- Bool -> RType RTyCon RTyVar r -> m (RType RTyCon RTyVar r)
forall (m :: * -> *) a. Freshable m a => Bool -> a -> m a
true Bool
allowTC RType RTyCon RTyVar r
tx
       RType RTyCon RTyVar r -> m (RType RTyCon RTyVar r)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (RType RTyCon RTyVar r -> m (RType RTyCon RTyVar r))
-> RType RTyCon RTyVar r -> m (RType RTyCon RTyVar r)
forall a b. (a -> b) -> a -> b
$ Symbol
-> RType RTyCon RTyVar r
-> RType RTyCon RTyVar r
-> RType RTyCon RTyVar r
forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> RType c tv r
RAllE Symbol
y' RType RTyCon RTyVar r
ty' (RType RTyCon RTyVar r
tx' RType RTyCon RTyVar r -> (Symbol, Expr) -> RType RTyCon RTyVar r
forall a. Subable a => a -> (Symbol, Expr) -> a
`F.subst1` (Symbol
y, Symbol -> Expr
F.EVar Symbol
y'))

trueRefType Bool
allowTC (RRTy [(Symbol, RType RTyCon RTyVar r)]
e r
o Oblig
r RType RTyCon RTyVar r
t)
  = [(Symbol, RType RTyCon RTyVar r)]
-> r -> Oblig -> RType RTyCon RTyVar r -> RType RTyCon RTyVar r
forall c tv r.
[(Symbol, RType c tv r)]
-> r -> Oblig -> RType c tv r -> RType c tv r
RRTy [(Symbol, RType RTyCon RTyVar r)]
e r
o Oblig
r (RType RTyCon RTyVar r -> RType RTyCon RTyVar r)
-> m (RType RTyCon RTyVar r) -> m (RType RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> RType RTyCon RTyVar r -> m (RType RTyCon RTyVar r)
forall (m :: * -> *) r.
(Freshable m Integer, Freshable m r, Reftable r) =>
Bool -> RRType r -> m (RRType r)
trueRefType Bool
allowTC RType RTyCon RTyVar r
t

trueRefType Bool
allowTC (REx Symbol
_ RType RTyCon RTyVar r
t RType RTyCon RTyVar r
t')
  = Symbol
-> RType RTyCon RTyVar r
-> RType RTyCon RTyVar r
-> RType RTyCon RTyVar r
forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> RType c tv r
REx (Symbol
 -> RType RTyCon RTyVar r
 -> RType RTyCon RTyVar r
 -> RType RTyCon RTyVar r)
-> m Symbol
-> m (RType RTyCon RTyVar r
      -> RType RTyCon RTyVar r -> RType RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Symbol
forall (m :: * -> *) a. Freshable m a => m a
fresh m (RType RTyCon RTyVar r
   -> RType RTyCon RTyVar r -> RType RTyCon RTyVar r)
-> m (RType RTyCon RTyVar r)
-> m (RType RTyCon RTyVar r -> RType RTyCon RTyVar r)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Bool -> RType RTyCon RTyVar r -> m (RType RTyCon RTyVar r)
forall (m :: * -> *) a. Freshable m a => Bool -> a -> m a
true Bool
allowTC RType RTyCon RTyVar r
t m (RType RTyCon RTyVar r -> RType RTyCon RTyVar r)
-> m (RType RTyCon RTyVar r) -> m (RType RTyCon RTyVar r)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Bool -> RType RTyCon RTyVar r -> m (RType RTyCon RTyVar r)
forall (m :: * -> *) a. Freshable m a => Bool -> a -> m a
true Bool
allowTC RType RTyCon RTyVar r
t'

trueRefType Bool
_ t :: RType RTyCon RTyVar r
t@(RExprArg Located Expr
_)
  = RType RTyCon RTyVar r -> m (RType RTyCon RTyVar r)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return RType RTyCon RTyVar r
t

trueRefType Bool
_ t :: RType RTyCon RTyVar r
t@(RHole r
_)
  = RType RTyCon RTyVar r -> m (RType RTyCon RTyVar r)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return RType RTyCon RTyVar r
t

trueRef :: (F.Reftable r, Freshable f r, Freshable f Integer)
        => Bool -> Ref τ (RType RTyCon RTyVar r) -> f (Ref τ (RRType r))
trueRef :: forall r (f :: * -> *) τ.
(Reftable r, Freshable f r, Freshable f Integer) =>
Bool
-> Ref τ (RType RTyCon RTyVar r)
-> f (Ref τ (RType RTyCon RTyVar r))
trueRef Bool
_ (RProp [(Symbol, τ)]
_ (RHole r
_)) = Maybe SrcSpan -> String -> f (Ref τ (RType RTyCon RTyVar r))
forall a. Maybe SrcSpan -> String -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing String
"trueRef: unexpected RProp _ (RHole _))"
trueRef Bool
allowTC (RProp [(Symbol, τ)]
s RType RTyCon RTyVar r
t) = [(Symbol, τ)]
-> RType RTyCon RTyVar r -> Ref τ (RType RTyCon RTyVar r)
forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp [(Symbol, τ)]
s (RType RTyCon RTyVar r -> Ref τ (RType RTyCon RTyVar r))
-> f (RType RTyCon RTyVar r) -> f (Ref τ (RType RTyCon RTyVar r))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> RType RTyCon RTyVar r -> f (RType RTyCon RTyVar r)
forall (m :: * -> *) r.
(Freshable m Integer, Freshable m r, Reftable r) =>
Bool -> RRType r -> m (RRType r)
trueRefType Bool
allowTC RType RTyCon RTyVar r
t


-----------------------------------------------------------------------------------------------
refreshRefType :: (Freshable m Integer, Freshable m r, F.Reftable r) => Bool -> RRType r -> m (RRType r)
-----------------------------------------------------------------------------------------------
refreshRefType :: forall (m :: * -> *) r.
(Freshable m Integer, Freshable m r, Reftable r) =>
Bool -> RRType r -> m (RRType r)
refreshRefType Bool
allowTC (RAllT RTVU RTyCon RTyVar
α RType RTyCon RTyVar r
t r
r)
  = RTVU RTyCon RTyVar
-> RType RTyCon RTyVar r -> r -> RType RTyCon RTyVar r
forall c tv r. RTVU c tv -> RType c tv r -> r -> RType c tv r
RAllT RTVU RTyCon RTyVar
α (RType RTyCon RTyVar r -> r -> RType RTyCon RTyVar r)
-> m (RType RTyCon RTyVar r) -> m (r -> RType RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> RType RTyCon RTyVar r -> m (RType RTyCon RTyVar r)
forall (m :: * -> *) a. Freshable m a => Bool -> a -> m a
refresh Bool
allowTC RType RTyCon RTyVar r
t m (r -> RType RTyCon RTyVar r) -> m r -> m (RType RTyCon RTyVar r)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Bool -> r -> m r
forall (m :: * -> *) a. Freshable m a => Bool -> a -> m a
true Bool
allowTC r
r

refreshRefType Bool
allowTC (RAllP PVU RTyCon RTyVar
π RType RTyCon RTyVar r
t)
  = PVU RTyCon RTyVar -> RType RTyCon RTyVar r -> RType RTyCon RTyVar r
forall c tv r. PVU c tv -> RType c tv r -> RType c tv r
RAllP PVU RTyCon RTyVar
π (RType RTyCon RTyVar r -> RType RTyCon RTyVar r)
-> m (RType RTyCon RTyVar r) -> m (RType RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> RType RTyCon RTyVar r -> m (RType RTyCon RTyVar r)
forall (m :: * -> *) a. Freshable m a => Bool -> a -> m a
refresh Bool
allowTC RType RTyCon RTyVar r
t

refreshRefType Bool
allowTC (RFun Symbol
sym RFInfo
i RType RTyCon RTyVar r
t RType RTyCon RTyVar r
t' r
_)
  | Symbol
sym Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
F.dummySymbol = (\Symbol
b RType RTyCon RTyVar r
t1 RType RTyCon RTyVar r
t2 -> Symbol
-> RFInfo
-> RType RTyCon RTyVar r
-> RType RTyCon RTyVar r
-> r
-> RType RTyCon RTyVar r
forall c tv r.
Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
b RFInfo
i RType RTyCon RTyVar r
t1 RType RTyCon RTyVar r
t2 r
forall a. Monoid a => a
mempty) (Symbol
 -> RType RTyCon RTyVar r
 -> RType RTyCon RTyVar r
 -> RType RTyCon RTyVar r)
-> m Symbol
-> m (RType RTyCon RTyVar r
      -> RType RTyCon RTyVar r -> RType RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Symbol
forall (m :: * -> *) a. Freshable m a => m a
fresh m (RType RTyCon RTyVar r
   -> RType RTyCon RTyVar r -> RType RTyCon RTyVar r)
-> m (RType RTyCon RTyVar r)
-> m (RType RTyCon RTyVar r -> RType RTyCon RTyVar r)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Bool -> RType RTyCon RTyVar r -> m (RType RTyCon RTyVar r)
forall (m :: * -> *) a. Freshable m a => Bool -> a -> m a
refresh Bool
allowTC RType RTyCon RTyVar r
t m (RType RTyCon RTyVar r -> RType RTyCon RTyVar r)
-> m (RType RTyCon RTyVar r) -> m (RType RTyCon RTyVar r)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Bool -> RType RTyCon RTyVar r -> m (RType RTyCon RTyVar r)
forall (m :: * -> *) a. Freshable m a => Bool -> a -> m a
refresh Bool
allowTC RType RTyCon RTyVar r
t'
  | Bool
otherwise          = (\RType RTyCon RTyVar r
t1 RType RTyCon RTyVar r
t2 -> Symbol
-> RFInfo
-> RType RTyCon RTyVar r
-> RType RTyCon RTyVar r
-> r
-> RType RTyCon RTyVar r
forall c tv r.
Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
sym RFInfo
i RType RTyCon RTyVar r
t1 RType RTyCon RTyVar r
t2 r
forall a. Monoid a => a
mempty)   (RType RTyCon RTyVar r
 -> RType RTyCon RTyVar r -> RType RTyCon RTyVar r)
-> m (RType RTyCon RTyVar r)
-> m (RType RTyCon RTyVar r -> RType RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> RType RTyCon RTyVar r -> m (RType RTyCon RTyVar r)
forall (m :: * -> *) a. Freshable m a => Bool -> a -> m a
refresh Bool
allowTC RType RTyCon RTyVar r
t m (RType RTyCon RTyVar r -> RType RTyCon RTyVar r)
-> m (RType RTyCon RTyVar r) -> m (RType RTyCon RTyVar r)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Bool -> RType RTyCon RTyVar r -> m (RType RTyCon RTyVar r)
forall (m :: * -> *) a. Freshable m a => Bool -> a -> m a
refresh Bool
allowTC RType RTyCon RTyVar r
t'

refreshRefType Bool
_ (RApp RTyCon
rc [RType RTyCon RTyVar r]
ts [RTProp RTyCon RTyVar r]
_ r
_) | RTyCon -> Bool
forall c. TyConable c => c -> Bool
isClass RTyCon
rc
  = RType RTyCon RTyVar r -> m (RType RTyCon RTyVar r)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (RType RTyCon RTyVar r -> m (RType RTyCon RTyVar r))
-> RType RTyCon RTyVar r -> m (RType RTyCon RTyVar r)
forall a b. (a -> b) -> a -> b
$ RTyCon -> [RType RTyCon RTyVar r] -> RType RTyCon RTyVar r
forall r c tv. Monoid r => c -> [RType c tv r] -> RType c tv r
rRCls RTyCon
rc [RType RTyCon RTyVar r]
ts

refreshRefType Bool
allowTC (RApp RTyCon
rc [RType RTyCon RTyVar r]
ts [RTProp RTyCon RTyVar r]
rs r
r)
  = RTyCon
-> [RType RTyCon RTyVar r]
-> [RTProp RTyCon RTyVar r]
-> r
-> RType RTyCon RTyVar r
forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp RTyCon
rc ([RType RTyCon RTyVar r]
 -> [RTProp RTyCon RTyVar r] -> r -> RType RTyCon RTyVar r)
-> m [RType RTyCon RTyVar r]
-> m ([RTProp RTyCon RTyVar r] -> r -> RType RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (RType RTyCon RTyVar r -> m (RType RTyCon RTyVar r))
-> [RType RTyCon RTyVar r] -> m [RType RTyCon RTyVar r]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Bool -> RType RTyCon RTyVar r -> m (RType RTyCon RTyVar r)
forall (m :: * -> *) a. Freshable m a => Bool -> a -> m a
refresh Bool
allowTC) [RType RTyCon RTyVar r]
ts m ([RTProp RTyCon RTyVar r] -> r -> RType RTyCon RTyVar r)
-> m [RTProp RTyCon RTyVar r] -> m (r -> RType RTyCon RTyVar r)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (RTProp RTyCon RTyVar r -> m (RTProp RTyCon RTyVar r))
-> [RTProp RTyCon RTyVar r] -> m [RTProp RTyCon RTyVar r]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Bool -> RTProp RTyCon RTyVar r -> m (RTProp RTyCon RTyVar r)
forall r (f :: * -> *) τ.
(Reftable r, Freshable f r, Freshable f Integer) =>
Bool
-> Ref τ (RType RTyCon RTyVar r)
-> f (Ref τ (RType RTyCon RTyVar r))
refreshRef Bool
allowTC) [RTProp RTyCon RTyVar r]
rs m (r -> RType RTyCon RTyVar r) -> m r -> m (RType RTyCon RTyVar r)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Bool -> r -> m r
forall (m :: * -> *) a. Freshable m a => Bool -> a -> m a
refresh Bool
allowTC r
r

refreshRefType Bool
allowTC (RVar RTyVar
a r
r)
  = RTyVar -> r -> RType RTyCon RTyVar r
forall c tv r. tv -> r -> RType c tv r
RVar RTyVar
a (r -> RType RTyCon RTyVar r) -> m r -> m (RType RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> r -> m r
forall (m :: * -> *) a. Freshable m a => Bool -> a -> m a
refresh Bool
allowTC r
r

refreshRefType Bool
allowTC (RAppTy RType RTyCon RTyVar r
t RType RTyCon RTyVar r
t' r
r)
  = RType RTyCon RTyVar r
-> RType RTyCon RTyVar r -> r -> RType RTyCon RTyVar r
forall c tv r. RType c tv r -> RType c tv r -> r -> RType c tv r
RAppTy (RType RTyCon RTyVar r
 -> RType RTyCon RTyVar r -> r -> RType RTyCon RTyVar r)
-> m (RType RTyCon RTyVar r)
-> m (RType RTyCon RTyVar r -> r -> RType RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> RType RTyCon RTyVar r -> m (RType RTyCon RTyVar r)
forall (m :: * -> *) a. Freshable m a => Bool -> a -> m a
refresh Bool
allowTC RType RTyCon RTyVar r
t m (RType RTyCon RTyVar r -> r -> RType RTyCon RTyVar r)
-> m (RType RTyCon RTyVar r) -> m (r -> RType RTyCon RTyVar r)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Bool -> RType RTyCon RTyVar r -> m (RType RTyCon RTyVar r)
forall (m :: * -> *) a. Freshable m a => Bool -> a -> m a
refresh Bool
allowTC RType RTyCon RTyVar r
t' m (r -> RType RTyCon RTyVar r) -> m r -> m (RType RTyCon RTyVar r)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Bool -> r -> m r
forall (m :: * -> *) a. Freshable m a => Bool -> a -> m a
refresh Bool
allowTC r
r

refreshRefType Bool
allowTC (RAllE Symbol
y RType RTyCon RTyVar r
ty RType RTyCon RTyVar r
tx)
  = do Symbol
y'  <- m Symbol
forall (m :: * -> *) a. Freshable m a => m a
fresh
       RType RTyCon RTyVar r
ty' <- Bool -> RType RTyCon RTyVar r -> m (RType RTyCon RTyVar r)
forall (m :: * -> *) a. Freshable m a => Bool -> a -> m a
refresh Bool
allowTC RType RTyCon RTyVar r
ty
       RType RTyCon RTyVar r
tx' <- Bool -> RType RTyCon RTyVar r -> m (RType RTyCon RTyVar r)
forall (m :: * -> *) a. Freshable m a => Bool -> a -> m a
refresh Bool
allowTC RType RTyCon RTyVar r
tx
       RType RTyCon RTyVar r -> m (RType RTyCon RTyVar r)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (RType RTyCon RTyVar r -> m (RType RTyCon RTyVar r))
-> RType RTyCon RTyVar r -> m (RType RTyCon RTyVar r)
forall a b. (a -> b) -> a -> b
$ Symbol
-> RType RTyCon RTyVar r
-> RType RTyCon RTyVar r
-> RType RTyCon RTyVar r
forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> RType c tv r
RAllE Symbol
y' RType RTyCon RTyVar r
ty' (RType RTyCon RTyVar r
tx' RType RTyCon RTyVar r -> (Symbol, Expr) -> RType RTyCon RTyVar r
forall a. Subable a => a -> (Symbol, Expr) -> a
`F.subst1` (Symbol
y, Symbol -> Expr
F.EVar Symbol
y'))

refreshRefType Bool
allowTC (RRTy [(Symbol, RType RTyCon RTyVar r)]
e r
o Oblig
r RType RTyCon RTyVar r
t)
  = [(Symbol, RType RTyCon RTyVar r)]
-> r -> Oblig -> RType RTyCon RTyVar r -> RType RTyCon RTyVar r
forall c tv r.
[(Symbol, RType c tv r)]
-> r -> Oblig -> RType c tv r -> RType c tv r
RRTy [(Symbol, RType RTyCon RTyVar r)]
e r
o Oblig
r (RType RTyCon RTyVar r -> RType RTyCon RTyVar r)
-> m (RType RTyCon RTyVar r) -> m (RType RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> RType RTyCon RTyVar r -> m (RType RTyCon RTyVar r)
forall (m :: * -> *) r.
(Freshable m Integer, Freshable m r, Reftable r) =>
Bool -> RRType r -> m (RRType r)
refreshRefType Bool
allowTC RType RTyCon RTyVar r
t

refreshRefType Bool
_ RType RTyCon RTyVar r
t
  = RType RTyCon RTyVar r -> m (RType RTyCon RTyVar r)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return RType RTyCon RTyVar r
t

refreshRef :: (F.Reftable r, Freshable f r, Freshable f Integer)
           => Bool -> Ref τ (RType RTyCon RTyVar r) -> f (Ref τ (RRType r))
refreshRef :: forall r (f :: * -> *) τ.
(Reftable r, Freshable f r, Freshable f Integer) =>
Bool
-> Ref τ (RType RTyCon RTyVar r)
-> f (Ref τ (RType RTyCon RTyVar r))
refreshRef Bool
_ (RProp [(Symbol, τ)]
_ (RHole r
_)) = Maybe SrcSpan -> String -> f (Ref τ (RType RTyCon RTyVar r))
forall a. Maybe SrcSpan -> String -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing String
"refreshRef: unexpected (RProp _ (RHole _))"
refreshRef Bool
allowTC (RProp [(Symbol, τ)]
s RType RTyCon RTyVar r
t) = [(Symbol, τ)]
-> RType RTyCon RTyVar r -> Ref τ (RType RTyCon RTyVar r)
forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp ([(Symbol, τ)]
 -> RType RTyCon RTyVar r -> Ref τ (RType RTyCon RTyVar r))
-> f [(Symbol, τ)]
-> f (RType RTyCon RTyVar r -> Ref τ (RType RTyCon RTyVar r))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Symbol, τ) -> f (Symbol, τ)) -> [(Symbol, τ)] -> f [(Symbol, τ)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Symbol, τ) -> f (Symbol, τ)
forall (f :: * -> *) a t t1. Freshable f a => (t, t1) -> f (a, t1)
freshSym [(Symbol, τ)]
s f (RType RTyCon RTyVar r -> Ref τ (RType RTyCon RTyVar r))
-> f (RType RTyCon RTyVar r) -> f (Ref τ (RType RTyCon RTyVar r))
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Bool -> RType RTyCon RTyVar r -> f (RType RTyCon RTyVar r)
forall (m :: * -> *) r.
(Freshable m Integer, Freshable m r, Reftable r) =>
Bool -> RRType r -> m (RRType r)
refreshRefType Bool
allowTC RType RTyCon RTyVar r
t

freshSym :: Freshable f a => (t, t1) -> f (a, t1)
freshSym :: forall (f :: * -> *) a t t1. Freshable f a => (t, t1) -> f (a, t1)
freshSym (t
_, t1
t)        = (, t1
t) (a -> (a, t1)) -> f a -> f (a, t1)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f a
forall (m :: * -> *) a. Freshable m a => m a
fresh


--------------------------------------------------------------------------------
refreshTy :: (FreshM m) => SpecType -> m SpecType
--------------------------------------------------------------------------------
refreshTy :: forall (m :: * -> *). FreshM m => SpecType -> m SpecType
refreshTy SpecType
t = SpecType -> m SpecType
forall (m :: * -> *). FreshM m => SpecType -> m SpecType
refreshVV SpecType
t m SpecType -> (SpecType -> m SpecType) -> m SpecType
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= SpecType -> m SpecType
forall (m :: * -> *). FreshM m => SpecType -> m SpecType
refreshArgs

--------------------------------------------------------------------------------
type FreshM m = Freshable m Integer
--------------------------------------------------------------------------------

--------------------------------------------------------------------------------
refreshVV :: FreshM m => SpecType -> m SpecType
--------------------------------------------------------------------------------
refreshVV :: forall (m :: * -> *). FreshM m => SpecType -> m SpecType
refreshVV (RAllT RTVU RTyCon RTyVar
a SpecType
t RReft
r) =
  RTVU RTyCon RTyVar -> SpecType -> RReft -> SpecType
forall c tv r. RTVU c tv -> RType c tv r -> r -> RType c tv r
RAllT RTVU RTyCon RTyVar
a (SpecType -> RReft -> SpecType)
-> m SpecType -> m (RReft -> SpecType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SpecType -> m SpecType
forall (m :: * -> *). FreshM m => SpecType -> m SpecType
refreshVV SpecType
t m (RReft -> SpecType) -> m RReft -> m SpecType
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> RReft -> m RReft
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return RReft
r

refreshVV (RAllP PVU RTyCon RTyVar
p SpecType
t) =
  PVU RTyCon RTyVar -> SpecType -> SpecType
forall c tv r. PVU c tv -> RType c tv r -> RType c tv r
RAllP PVU RTyCon RTyVar
p (SpecType -> SpecType) -> m SpecType -> m SpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SpecType -> m SpecType
forall (m :: * -> *). FreshM m => SpecType -> m SpecType
refreshVV SpecType
t

refreshVV (REx Symbol
x SpecType
t1 SpecType
t2) = do
  SpecType
t1' <- SpecType -> m SpecType
forall (m :: * -> *). FreshM m => SpecType -> m SpecType
refreshVV SpecType
t1
  SpecType
t2' <- SpecType -> m SpecType
forall (m :: * -> *). FreshM m => SpecType -> m SpecType
refreshVV SpecType
t2
  SpecType -> Symbol -> SpecType
forall c (f :: * -> *) tv.
(TyConable c, Reftable (f Reft), Functor f) =>
RType c tv (f Reft) -> Symbol -> RType c tv (f Reft)
shiftVV (Symbol -> SpecType -> SpecType -> SpecType
forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> RType c tv r
REx Symbol
x SpecType
t1' SpecType
t2') (Symbol -> SpecType) -> m Symbol -> m SpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Symbol
forall (m :: * -> *) a. Freshable m a => m a
fresh

refreshVV (RFun Symbol
x RFInfo
i SpecType
t1 SpecType
t2 RReft
r) = do
  SpecType
t1' <- SpecType -> m SpecType
forall (m :: * -> *). FreshM m => SpecType -> m SpecType
refreshVV SpecType
t1
  SpecType
t2' <- SpecType -> m SpecType
forall (m :: * -> *). FreshM m => SpecType -> m SpecType
refreshVV SpecType
t2
  SpecType -> Symbol -> SpecType
forall c (f :: * -> *) tv.
(TyConable c, Reftable (f Reft), Functor f) =>
RType c tv (f Reft) -> Symbol -> RType c tv (f Reft)
shiftVV (Symbol -> RFInfo -> SpecType -> SpecType -> RReft -> SpecType
forall c tv r.
Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
x RFInfo
i SpecType
t1' SpecType
t2' RReft
r) (Symbol -> SpecType) -> m Symbol -> m SpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Symbol
forall (m :: * -> *) a. Freshable m a => m a
fresh

refreshVV (RAppTy SpecType
t1 SpecType
t2 RReft
r) = do
  SpecType
t1' <- SpecType -> m SpecType
forall (m :: * -> *). FreshM m => SpecType -> m SpecType
refreshVV SpecType
t1
  SpecType
t2' <- SpecType -> m SpecType
forall (m :: * -> *). FreshM m => SpecType -> m SpecType
refreshVV SpecType
t2
  SpecType -> Symbol -> SpecType
forall c (f :: * -> *) tv.
(TyConable c, Reftable (f Reft), Functor f) =>
RType c tv (f Reft) -> Symbol -> RType c tv (f Reft)
shiftVV (SpecType -> SpecType -> RReft -> SpecType
forall c tv r. RType c tv r -> RType c tv r -> r -> RType c tv r
RAppTy SpecType
t1' SpecType
t2' RReft
r) (Symbol -> SpecType) -> m Symbol -> m SpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Symbol
forall (m :: * -> *) a. Freshable m a => m a
fresh

refreshVV (RApp RTyCon
c [SpecType]
ts [RTProp RTyCon RTyVar RReft]
rs RReft
r) = do
  [SpecType]
ts' <- (SpecType -> m SpecType) -> [SpecType] -> m [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 -> m SpecType
forall (m :: * -> *). FreshM m => SpecType -> m SpecType
refreshVV    [SpecType]
ts
  [RTProp RTyCon RTyVar RReft]
rs' <- (RTProp RTyCon RTyVar RReft -> m (RTProp RTyCon RTyVar RReft))
-> [RTProp RTyCon RTyVar RReft] -> m [RTProp RTyCon RTyVar RReft]
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 RTProp RTyCon RTyVar RReft -> m (RTProp RTyCon RTyVar RReft)
forall (m :: * -> *) b.
Freshable m Integer =>
Ref b SpecType -> m (Ref b SpecType)
refreshVVRef [RTProp RTyCon RTyVar RReft]
rs
  SpecType -> Symbol -> SpecType
forall c (f :: * -> *) tv.
(TyConable c, Reftable (f Reft), Functor f) =>
RType c tv (f Reft) -> Symbol -> RType c tv (f Reft)
shiftVV (RTyCon
-> [SpecType] -> [RTProp RTyCon RTyVar RReft] -> RReft -> SpecType
forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp RTyCon
c [SpecType]
ts' [RTProp RTyCon RTyVar RReft]
rs' RReft
r) (Symbol -> SpecType) -> m Symbol -> m SpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Symbol
forall (m :: * -> *) a. Freshable m a => m a
fresh

refreshVV SpecType
t =
  SpecType -> Symbol -> SpecType
forall c (f :: * -> *) tv.
(TyConable c, Reftable (f Reft), Functor f) =>
RType c tv (f Reft) -> Symbol -> RType c tv (f Reft)
shiftVV SpecType
t (Symbol -> SpecType) -> m Symbol -> m SpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Symbol
forall (m :: * -> *) a. Freshable m a => m a
fresh

refreshVVRef :: Freshable m Integer => Ref b SpecType -> m (Ref b SpecType)
refreshVVRef :: forall (m :: * -> *) b.
Freshable m Integer =>
Ref b SpecType -> m (Ref b SpecType)
refreshVVRef (RProp [(Symbol, b)]
ss (RHole RReft
r))
  = Ref b SpecType -> m (Ref b SpecType)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Ref b SpecType -> m (Ref b SpecType))
-> Ref b SpecType -> m (Ref b SpecType)
forall a b. (a -> b) -> a -> b
$ [(Symbol, b)] -> SpecType -> Ref b SpecType
forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp [(Symbol, b)]
ss (RReft -> SpecType
forall c tv r. r -> RType c tv r
RHole RReft
r)

refreshVVRef (RProp [(Symbol, b)]
ss SpecType
t)
  = do [Symbol]
xs    <- (Symbol -> m Symbol) -> [Symbol] -> m [Symbol]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (m Symbol -> Symbol -> m Symbol
forall a b. a -> b -> a
const m Symbol
forall (m :: * -> *) a. Freshable m a => m a
fresh) [Symbol]
syms
       let su :: Subst
su = [(Symbol, Expr)] -> Subst
F.mkSubst ([(Symbol, Expr)] -> Subst) -> [(Symbol, Expr)] -> Subst
forall a b. (a -> b) -> a -> b
$ [Symbol] -> [Expr] -> [(Symbol, Expr)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
syms (Symbol -> Expr
F.EVar (Symbol -> Expr) -> [Symbol] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
xs)
       SpecType
t'    <- SpecType -> m SpecType
forall (m :: * -> *). FreshM m => SpecType -> m SpecType
refreshVV SpecType
t
       Ref b SpecType -> m (Ref b SpecType)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Ref b SpecType -> m (Ref b SpecType))
-> Ref b SpecType -> m (Ref b SpecType)
forall a b. (a -> b) -> a -> b
$ [(Symbol, b)] -> SpecType -> Ref b SpecType
forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp ([Symbol] -> [b] -> [(Symbol, b)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
xs [b]
bs) (Subst -> SpecType -> SpecType
forall a. Subable a => Subst -> a -> a
F.subst Subst
su SpecType
t')
    where
    ([Symbol]
syms, [b]
bs) = [(Symbol, b)] -> ([Symbol], [b])
forall a b. [(a, b)] -> ([a], [b])
unzip [(Symbol, b)]
ss

--------------------------------------------------------------------------------
refreshArgs :: (FreshM m) => SpecType -> m SpecType
--------------------------------------------------------------------------------
refreshArgs :: forall (m :: * -> *). FreshM m => SpecType -> m SpecType
refreshArgs SpecType
t = (SpecType, Subst) -> SpecType
forall a b. (a, b) -> a
fst ((SpecType, Subst) -> SpecType)
-> m (SpecType, Subst) -> m SpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SpecType -> m (SpecType, Subst)
forall (m :: * -> *). FreshM m => SpecType -> m (SpecType, Subst)
refreshArgsSub SpecType
t


-- NV TODO: this does not refresh args if they are wrapped in an RRTy
refreshArgsSub :: (FreshM m) => SpecType -> m (SpecType, F.Subst)
refreshArgsSub :: forall (m :: * -> *). FreshM m => SpecType -> m (SpecType, Subst)
refreshArgsSub SpecType
t
  = do [SpecType]
ts     <- (SpecType -> m SpecType) -> [SpecType] -> m [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 -> m SpecType
forall (m :: * -> *). FreshM m => SpecType -> m SpecType
refreshArgs [SpecType]
ts_u
       [Symbol]
xs'    <- (Symbol -> m Symbol) -> [Symbol] -> m [Symbol]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (m Symbol -> Symbol -> m Symbol
forall a b. a -> b -> a
const m Symbol
forall (m :: * -> *) a. Freshable m a => m a
fresh) [Symbol]
xs
       let sus :: [Subst]
sus = [(Symbol, Expr)] -> Subst
F.mkSubst ([(Symbol, Expr)] -> Subst) -> [[(Symbol, Expr)]] -> [Subst]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, Expr)] -> [[(Symbol, Expr)]]
forall a. [a] -> [[a]]
L.inits ([Symbol] -> [Expr] -> [(Symbol, Expr)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
xs (Symbol -> Expr
F.EVar (Symbol -> Expr) -> [Symbol] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
xs'))
       let su :: Subst
su  = [Subst] -> Subst
forall a. HasCallStack => [a] -> a
last [Subst]
sus
       [SpecType]
ts'    <- (SpecType -> m SpecType) -> [SpecType] -> m [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 -> m SpecType
forall (m :: * -> *). FreshM m => SpecType -> m SpecType
refreshPs ([SpecType] -> m [SpecType]) -> [SpecType] -> m [SpecType]
forall a b. (a -> b) -> a -> b
$ (Subst -> SpecType -> SpecType)
-> [Subst] -> [SpecType] -> [SpecType]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Subst -> SpecType -> SpecType
forall a. Subable a => Subst -> a -> a
F.subst [Subst]
sus [SpecType]
ts
       let rs' :: [RReft]
rs' = (Subst -> RReft -> RReft) -> [Subst] -> [RReft] -> [RReft]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Subst -> RReft -> RReft
forall a. Subable a => Subst -> a -> a
F.subst [Subst]
sus [RReft]
rs
       SpecType
tr     <- SpecType -> m SpecType
forall (m :: * -> *). FreshM m => SpecType -> m SpecType
refreshPs (SpecType -> m SpecType) -> SpecType -> m SpecType
forall a b. (a -> b) -> a -> b
$ Subst -> SpecType -> SpecType
forall a. Subable a => Subst -> a -> a
F.subst Subst
su SpecType
tbd
       let t' :: SpecType
t'  = 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', ty_res = tr, ty_refts = rs'}
       (SpecType, Subst) -> m (SpecType, Subst)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SpecType
t', Subst
su)
    where
       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
t
       xs :: [Symbol]
xs      = RTypeRep RTyCon RTyVar RReft -> [Symbol]
forall c tv r. RTypeRep c tv r -> [Symbol]
ty_binds RTypeRep RTyCon RTyVar RReft
trep
       ts_u :: [SpecType]
ts_u    = RTypeRep RTyCon RTyVar RReft -> [SpecType]
forall c tv r. RTypeRep c tv r -> [RType c tv r]
ty_args  RTypeRep RTyCon RTyVar RReft
trep
       tbd :: SpecType
tbd     = RTypeRep RTyCon RTyVar RReft -> SpecType
forall c tv r. RTypeRep c tv r -> RType c tv r
ty_res   RTypeRep RTyCon RTyVar RReft
trep
       rs :: [RReft]
rs      = RTypeRep RTyCon RTyVar RReft -> [RReft]
forall c tv r. RTypeRep c tv r -> [r]
ty_refts RTypeRep RTyCon RTyVar RReft
trep

refreshPs :: (FreshM m) => SpecType -> m SpecType
refreshPs :: forall (m :: * -> *). FreshM m => SpecType -> m SpecType
refreshPs = (RTProp RTyCon RTyVar RReft -> m (RTProp RTyCon RTyVar RReft))
-> SpecType -> m SpecType
forall (m :: * -> *) c tv r.
Monad m =>
(RTProp c tv r -> m (RTProp c tv r))
-> RType c tv r -> m (RType c tv r)
mapPropM RTProp RTyCon RTyVar RReft -> m (RTProp RTyCon RTyVar RReft)
forall (m :: * -> *) b.
Freshable m Integer =>
Ref b SpecType -> m (Ref b SpecType)
go
  where
    go :: Ref τ SpecType -> m (Ref τ SpecType)
go (RProp [(Symbol, τ)]
s SpecType
st) = do
      SpecType
t'    <- SpecType -> m SpecType
forall (m :: * -> *). FreshM m => SpecType -> m SpecType
refreshPs SpecType
st
      [Symbol]
xs    <- ((Symbol, τ) -> m Symbol) -> [(Symbol, τ)] -> m [Symbol]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (m Symbol -> (Symbol, τ) -> m Symbol
forall a b. a -> b -> a
const m Symbol
forall (m :: * -> *) a. Freshable m a => m a
fresh) [(Symbol, τ)]
s
      let su :: Subst
su = [(Symbol, Expr)] -> Subst
F.mkSubst [(Symbol
y, Symbol -> Expr
F.EVar Symbol
x) | (Symbol
x, (Symbol
y, τ
_)) <- [Symbol] -> [(Symbol, τ)] -> [(Symbol, (Symbol, τ))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
xs [(Symbol, τ)]
s]
      Ref τ SpecType -> m (Ref τ SpecType)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Ref τ SpecType -> m (Ref τ SpecType))
-> Ref τ SpecType -> m (Ref τ SpecType)
forall a b. (a -> b) -> a -> b
$ [(Symbol, τ)] -> SpecType -> Ref τ SpecType
forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp [(Symbol
x, τ
t) | (Symbol
x, (Symbol
_, τ
t)) <- [Symbol] -> [(Symbol, τ)] -> [(Symbol, (Symbol, τ))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
xs [(Symbol, τ)]
s] (SpecType -> Ref τ SpecType) -> SpecType -> Ref τ SpecType
forall a b. (a -> b) -> a -> b
$ Subst -> SpecType -> SpecType
forall a. Subable a => Subst -> a -> a
F.subst Subst
su SpecType
t'

--------------------------------------------------------------------------------
refreshHoles :: (F.Symbolic t, F.Reftable r, TyConable c, Freshable f r)
             => Bool -> [(t, RType c tv r)] -> f ([F.Symbol], [(t, RType c tv r)])
refreshHoles :: forall t r c (f :: * -> *) tv.
(Symbolic t, Reftable r, TyConable c, Freshable f r) =>
Bool -> [(t, RType c tv r)] -> f ([Symbol], [(t, RType c tv r)])
refreshHoles Bool
allowTC [(t, RType c tv r)]
vts = ([Maybe Symbol] -> [Symbol])
-> ([Maybe Symbol], [(t, RType c tv r)])
-> ([Symbol], [(t, RType c tv r)])
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first [Maybe Symbol] -> [Symbol]
forall a. [Maybe a] -> [a]
catMaybes (([Maybe Symbol], [(t, RType c tv r)])
 -> ([Symbol], [(t, RType c tv r)]))
-> ([(Maybe Symbol, t, RType c tv r)]
    -> ([Maybe Symbol], [(t, RType c tv r)]))
-> [(Maybe Symbol, t, RType c tv r)]
-> ([Symbol], [(t, RType c tv r)])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Maybe Symbol, (t, RType c tv r))]
-> ([Maybe Symbol], [(t, RType c tv r)])
forall a b. [(a, b)] -> ([a], [b])
unzip ([(Maybe Symbol, (t, RType c tv r))]
 -> ([Maybe Symbol], [(t, RType c tv r)]))
-> ([(Maybe Symbol, t, RType c tv r)]
    -> [(Maybe Symbol, (t, RType c tv r))])
-> [(Maybe Symbol, t, RType c tv r)]
-> ([Maybe Symbol], [(t, RType c tv r)])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Maybe Symbol, t, RType c tv r)
 -> (Maybe Symbol, (t, RType c tv r)))
-> [(Maybe Symbol, t, RType c tv r)]
-> [(Maybe Symbol, (t, RType c tv r))]
forall a b. (a -> b) -> [a] -> [b]
map (Maybe Symbol, t, RType c tv r)
-> (Maybe Symbol, (t, RType c tv r))
forall {a} {a} {b}. (a, a, b) -> (a, (a, b))
extract ([(Maybe Symbol, t, RType c tv r)]
 -> ([Symbol], [(t, RType c tv r)]))
-> f [(Maybe Symbol, t, RType c tv r)]
-> f ([Symbol], [(t, RType c tv r)])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((t, RType c tv r) -> f (Maybe Symbol, t, RType c tv r))
-> [(t, RType c tv r)] -> f [(Maybe Symbol, t, RType c tv r)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Bool -> (t, RType c tv r) -> f (Maybe Symbol, t, RType c tv r)
forall a r c (m :: * -> *) tv.
(Symbolic a, Reftable r, TyConable c, Freshable m r) =>
Bool -> (a, RType c tv r) -> m (Maybe Symbol, a, RType c tv r)
refreshHoles' Bool
allowTC) [(t, RType c tv r)]
vts
  where
  --   extract :: (t, t1, t2) -> (t, (t1, t2))
    extract :: (a, a, b) -> (a, (a, b))
extract (a
a,a
b,b
c) = (a
a,(a
b,b
c))

refreshHoles' :: (F.Symbolic a, F.Reftable r, TyConable c, Freshable m r)
              => Bool -> (a, RType c tv r) -> m (Maybe F.Symbol, a, RType c tv r)
refreshHoles' :: forall a r c (m :: * -> *) tv.
(Symbolic a, Reftable r, TyConable c, Freshable m r) =>
Bool -> (a, RType c tv r) -> m (Maybe Symbol, a, RType c tv r)
refreshHoles' Bool
allowTC (a
x,RType c tv r
t)
  | RType c tv r -> Bool
forall r c tv. (Reftable r, TyConable c) => RType c tv r -> Bool
noHoles RType c tv r
t = (Maybe Symbol, a, RType c tv r)
-> m (Maybe Symbol, a, RType c tv r)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Symbol
forall a. Maybe a
Nothing, a
x, RType c tv r
t)
  | Bool
otherwise = (Symbol -> Maybe Symbol
forall a. a -> Maybe a
Just (Symbol -> Maybe Symbol) -> Symbol -> Maybe Symbol
forall a b. (a -> b) -> a -> b
$ a -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol a
x,a
x,) (RType c tv r -> (Maybe Symbol, a, RType c tv r))
-> m (RType c tv r) -> m (Maybe Symbol, a, RType c tv r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (r -> m r) -> RType c tv r -> m (RType c tv r)
forall (m :: * -> *) r1 r2 c tv.
Monad m =>
(r1 -> m r2) -> RType c tv r1 -> m (RType c tv r2)
mapReftM r -> m r
forall {a} {m :: * -> *}. (Reftable a, Freshable m a) => a -> m a
tx RType c tv r
t
  where
    tx :: a -> m a
tx a
r | a -> Bool
forall r. Reftable r => r -> Bool
hasHole a
r = Bool -> a -> m a
forall (m :: * -> *) a. Freshable m a => Bool -> a -> m a
refresh Bool
allowTC a
r
         | Bool
otherwise = a -> m a
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
r

noHoles :: (F.Reftable r, TyConable c) => RType c tv r -> Bool
noHoles :: forall r c tv. (Reftable r, TyConable c) => RType c tv r -> Bool
noHoles = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ([Bool] -> Bool)
-> (RType c tv r -> [Bool]) -> RType c tv r -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool
-> (SEnv (RType c tv r) -> r -> [Bool] -> [Bool])
-> [Bool]
-> RType c tv r
-> [Bool]
forall r c tv a.
(Reftable r, TyConable c) =>
Bool
-> (SEnv (RType c tv r) -> r -> a -> a) -> a -> RType c tv r -> a
foldReft Bool
False (\SEnv (RType c tv r)
_ r
r [Bool]
bs -> Bool -> Bool
not (r -> Bool
forall r. Reftable r => r -> Bool
hasHole r
r) Bool -> [Bool] -> [Bool]
forall a. a -> [a] -> [a]
: [Bool]
bs) []