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

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.Errors
import           Language.Haskell.Liquid.Types.RType
import           Language.Haskell.Liquid.Types.RTypeOp
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
forall {b} {v}. Monoid (KVarSubst b v) => Integer -> ExprBV b v
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 -> ExprBV b v
kv Integer
i = KVar -> HashMap Symbol Sort -> KVarSubst b v -> ExprBV b v
forall b v.
KVar -> HashMap Symbol Sort -> KVarSubst b v -> ExprBV b v
F.PKVar (Integer -> KVar
F.intKvar Integer
i) HashMap Symbol Sort
forall a. Monoid a => a
mempty KVarSubst b v
forall a. Monoid a => a
mempty

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. HasCallStack => 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
forall b v. (b, ExprBV b v) -> ReftBV b v
F.Reft (Symbol
v, Expr
forall b v. ExprBV b v
F.PTrue)
  refresh :: Bool -> Reft -> m Reft
refresh Bool
_ (F.Reft (Symbol
_,Expr
_)) = ((Symbol, Expr) -> Reft
forall b v. (b, ExprBV b v) -> ReftBV b v
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. HasCallStack => 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 PredicateBV Symbol Symbol
_)    = Reft -> PredicateBV Symbol Symbol -> RReft
forall b v r. r -> PredicateBV b v -> UReftBV b v r
MkUReft (Reft -> PredicateBV Symbol Symbol -> RReft)
-> m Reft -> m (PredicateBV Symbol Symbol -> 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 (PredicateBV Symbol Symbol -> RReft)
-> m (PredicateBV Symbol Symbol) -> 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
<*> PredicateBV Symbol Symbol -> m (PredicateBV Symbol Symbol)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return PredicateBV Symbol Symbol
forall a. Monoid a => a
mempty
  refresh :: Bool -> RReft -> m RReft
refresh Bool
allowTC (MkUReft Reft
r PredicateBV Symbol Symbol
_) = Reft -> PredicateBV Symbol Symbol -> RReft
forall b v r. r -> PredicateBV b v -> UReftBV b v r
MkUReft (Reft -> PredicateBV Symbol Symbol -> RReft)
-> m Reft -> m (PredicateBV Symbol Symbol -> 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 (PredicateBV Symbol Symbol -> RReft)
-> m (PredicateBV Symbol Symbol) -> 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
<*> PredicateBV Symbol Symbol -> m (PredicateBV Symbol Symbol)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return PredicateBV Symbol Symbol
forall a. Monoid a => a
mempty

instance (Freshable m Integer, Freshable m r, IsReft r, F.Subable r, F.Variable r ~ F.Symbol, ReftBind r ~ F.Symbol, ReftVar r ~ F.Symbol) => Freshable m (RRType r) where
  fresh :: m (RRType r)
fresh   = Maybe SrcSpan -> String -> m (RRType r)
forall a. HasCallStack => 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, IsReft r, Subable r,
 Variable r ~ Symbol, ReftBind r ~ Symbol, ReftVar r ~ Symbol) =>
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, IsReft r, Subable r,
 Variable r ~ Symbol, ReftBind r ~ Symbol, ReftVar r ~ Symbol) =>
Bool -> RRType r -> m (RRType r)
trueRefType

-----------------------------------------------------------------------------------------------
trueRefType :: (Freshable m Integer, Freshable m r, IsReft r, F.Subable r, F.Variable r ~ F.Symbol, ReftBind r ~ F.Symbol, ReftVar r ~ F.Symbol) => Bool -> RRType r -> m (RRType r)
-----------------------------------------------------------------------------------------------
trueRefType :: forall (m :: * -> *) r.
(Freshable m Integer, Freshable m r, IsReft r, Subable r,
 Variable r ~ Symbol, ReftBind r ~ Symbol, ReftVar r ~ Symbol) =>
Bool -> RRType r -> m (RRType r)
trueRefType Bool
allowTC (RAllT RTVUBV Symbol Symbol RTyCon RTyVar
α RTypeBV Symbol Symbol RTyCon RTyVar r
t r
r)
  = RTVUBV Symbol Symbol RTyCon RTyVar
-> RTypeBV Symbol Symbol RTyCon RTyVar r
-> r
-> RTypeBV Symbol Symbol RTyCon RTyVar r
forall b v c tv r.
RTVUBV b v c tv -> RTypeBV b v c tv r -> r -> RTypeBV b v c tv r
RAllT RTVUBV Symbol Symbol RTyCon RTyVar
α (RTypeBV Symbol Symbol RTyCon RTyVar r
 -> r -> RTypeBV Symbol Symbol RTyCon RTyVar r)
-> m (RTypeBV Symbol Symbol RTyCon RTyVar r)
-> m (r -> RTypeBV Symbol Symbol RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool
-> RTypeBV Symbol Symbol RTyCon RTyVar r
-> m (RTypeBV Symbol Symbol RTyCon RTyVar r)
forall (m :: * -> *) a. Freshable m a => Bool -> a -> m a
true Bool
allowTC RTypeBV Symbol Symbol RTyCon RTyVar r
t m (r -> RTypeBV Symbol Symbol RTyCon RTyVar r)
-> m r -> m (RTypeBV Symbol Symbol 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 PVUBV Symbol Symbol RTyCon RTyVar
π RTypeBV Symbol Symbol RTyCon RTyVar r
t)
  = PVUBV Symbol Symbol RTyCon RTyVar
-> RTypeBV Symbol Symbol RTyCon RTyVar r
-> RTypeBV Symbol Symbol RTyCon RTyVar r
forall b v c tv r.
PVUBV b v c tv -> RTypeBV b v c tv r -> RTypeBV b v c tv r
RAllP PVUBV Symbol Symbol RTyCon RTyVar
π (RTypeBV Symbol Symbol RTyCon RTyVar r
 -> RTypeBV Symbol Symbol RTyCon RTyVar r)
-> m (RTypeBV Symbol Symbol RTyCon RTyVar r)
-> m (RTypeBV Symbol Symbol RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool
-> RTypeBV Symbol Symbol RTyCon RTyVar r
-> m (RTypeBV Symbol Symbol RTyCon RTyVar r)
forall (m :: * -> *) a. Freshable m a => Bool -> a -> m a
true Bool
allowTC RTypeBV Symbol Symbol RTyCon RTyVar r
t

trueRefType Bool
allowTC (RFun Symbol
_ RFInfo
_ RTypeBV Symbol Symbol RTyCon RTyVar r
t RTypeBV Symbol Symbol RTyCon RTyVar r
t' r
_)
  -- YL: attaching rfinfo here is crucial
  = RFInfo
-> Symbol
-> RTypeBV Symbol Symbol RTyCon RTyVar r
-> RTypeBV Symbol Symbol RTyCon RTyVar r
-> RTypeBV Symbol Symbol RTyCon RTyVar r
forall r c tv.
IsReft r =>
RFInfo -> Symbol -> RType c tv r -> RType c tv r -> RType c tv r
rFun' (Bool -> RFInfo
classRFInfo Bool
allowTC) (Symbol
 -> RTypeBV Symbol Symbol RTyCon RTyVar r
 -> RTypeBV Symbol Symbol RTyCon RTyVar r
 -> RTypeBV Symbol Symbol RTyCon RTyVar r)
-> m Symbol
-> m (RTypeBV Symbol Symbol RTyCon RTyVar r
      -> RTypeBV Symbol Symbol RTyCon RTyVar r
      -> RTypeBV Symbol Symbol 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 (RTypeBV Symbol Symbol RTyCon RTyVar r
   -> RTypeBV Symbol Symbol RTyCon RTyVar r
   -> RTypeBV Symbol Symbol RTyCon RTyVar r)
-> m (RTypeBV Symbol Symbol RTyCon RTyVar r)
-> m (RTypeBV Symbol Symbol RTyCon RTyVar r
      -> RTypeBV Symbol Symbol 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
-> RTypeBV Symbol Symbol RTyCon RTyVar r
-> m (RTypeBV Symbol Symbol RTyCon RTyVar r)
forall (m :: * -> *) a. Freshable m a => Bool -> a -> m a
true Bool
allowTC RTypeBV Symbol Symbol RTyCon RTyVar r
t m (RTypeBV Symbol Symbol RTyCon RTyVar r
   -> RTypeBV Symbol Symbol RTyCon RTyVar r)
-> m (RTypeBV Symbol Symbol RTyCon RTyVar r)
-> m (RTypeBV Symbol Symbol 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
-> RTypeBV Symbol Symbol RTyCon RTyVar r
-> m (RTypeBV Symbol Symbol RTyCon RTyVar r)
forall (m :: * -> *) a. Freshable m a => Bool -> a -> m a
true Bool
allowTC RTypeBV Symbol Symbol RTyCon RTyVar r
t'

trueRefType Bool
allowTC (RApp RTyCon
c [RTypeBV Symbol Symbol RTyCon RTyVar r]
ts [RTPropBV Symbol Symbol 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
-> [RTypeBV Symbol Symbol RTyCon RTyVar r]
-> RTypeBV Symbol Symbol RTyCon RTyVar r
forall r c tv. IsReft r => c -> [RType c tv r] -> RType c tv r
rRCls RTyCon
c ([RTypeBV Symbol Symbol RTyCon RTyVar r]
 -> RTypeBV Symbol Symbol RTyCon RTyVar r)
-> m [RTypeBV Symbol Symbol RTyCon RTyVar r]
-> m (RTypeBV Symbol Symbol RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (RTypeBV Symbol Symbol RTyCon RTyVar r
 -> m (RTypeBV Symbol Symbol RTyCon RTyVar r))
-> [RTypeBV Symbol Symbol RTyCon RTyVar r]
-> m [RTypeBV Symbol Symbol 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
-> RTypeBV Symbol Symbol RTyCon RTyVar r
-> m (RTypeBV Symbol Symbol RTyCon RTyVar r)
forall (m :: * -> *) a. Freshable m a => Bool -> a -> m a
true Bool
allowTC) [RTypeBV Symbol Symbol RTyCon RTyVar r]
ts

trueRefType Bool
allowTC (RApp RTyCon
c [RTypeBV Symbol Symbol RTyCon RTyVar r]
ts [RTPropBV Symbol Symbol RTyCon RTyVar r]
rs r
r)
  = RTyCon
-> [RTypeBV Symbol Symbol RTyCon RTyVar r]
-> [RTPropBV Symbol Symbol RTyCon RTyVar r]
-> r
-> RTypeBV Symbol Symbol RTyCon RTyVar r
forall b v c tv r.
c
-> [RTypeBV b v c tv r]
-> [RTPropBV b v c tv r]
-> r
-> RTypeBV b v c tv r
RApp RTyCon
c ([RTypeBV Symbol Symbol RTyCon RTyVar r]
 -> [RTPropBV Symbol Symbol RTyCon RTyVar r]
 -> r
 -> RTypeBV Symbol Symbol RTyCon RTyVar r)
-> m [RTypeBV Symbol Symbol RTyCon RTyVar r]
-> m ([RTPropBV Symbol Symbol RTyCon RTyVar r]
      -> r -> RTypeBV Symbol Symbol RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (RTypeBV Symbol Symbol RTyCon RTyVar r
 -> m (RTypeBV Symbol Symbol RTyCon RTyVar r))
-> [RTypeBV Symbol Symbol RTyCon RTyVar r]
-> m [RTypeBV Symbol Symbol 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
-> RTypeBV Symbol Symbol RTyCon RTyVar r
-> m (RTypeBV Symbol Symbol RTyCon RTyVar r)
forall (m :: * -> *) a. Freshable m a => Bool -> a -> m a
true Bool
allowTC) [RTypeBV Symbol Symbol RTyCon RTyVar r]
ts m ([RTPropBV Symbol Symbol RTyCon RTyVar r]
   -> r -> RTypeBV Symbol Symbol RTyCon RTyVar r)
-> m [RTPropBV Symbol Symbol RTyCon RTyVar r]
-> m (r -> RTypeBV Symbol Symbol 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
<*> (RTPropBV Symbol Symbol RTyCon RTyVar r
 -> m (RTPropBV Symbol Symbol RTyCon RTyVar r))
-> [RTPropBV Symbol Symbol RTyCon RTyVar r]
-> m [RTPropBV Symbol Symbol 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
-> RTPropBV Symbol Symbol RTyCon RTyVar r
-> m (RTPropBV Symbol Symbol RTyCon RTyVar r)
forall (f :: * -> *) r τ.
(Freshable f Integer, Freshable f r, IsReft r, Subable r,
 Variable r ~ Symbol, ReftBind r ~ Symbol, ReftVar r ~ Symbol) =>
Bool
-> Ref τ (RType RTyCon RTyVar r)
-> f (Ref τ (RType RTyCon RTyVar r))
trueRef Bool
allowTC) [RTPropBV Symbol Symbol RTyCon RTyVar r]
rs m (r -> RTypeBV Symbol Symbol RTyCon RTyVar r)
-> m r -> m (RTypeBV Symbol Symbol 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 RTypeBV Symbol Symbol RTyCon RTyVar r
t RTypeBV Symbol Symbol RTyCon RTyVar r
t' r
_)
  = RTypeBV Symbol Symbol RTyCon RTyVar r
-> RTypeBV Symbol Symbol RTyCon RTyVar r
-> r
-> RTypeBV Symbol Symbol RTyCon RTyVar r
forall b v c tv r.
RTypeBV b v c tv r -> RTypeBV b v c tv r -> r -> RTypeBV b v c tv r
RAppTy (RTypeBV Symbol Symbol RTyCon RTyVar r
 -> RTypeBV Symbol Symbol RTyCon RTyVar r
 -> r
 -> RTypeBV Symbol Symbol RTyCon RTyVar r)
-> m (RTypeBV Symbol Symbol RTyCon RTyVar r)
-> m (RTypeBV Symbol Symbol RTyCon RTyVar r
      -> r -> RTypeBV Symbol Symbol RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool
-> RTypeBV Symbol Symbol RTyCon RTyVar r
-> m (RTypeBV Symbol Symbol RTyCon RTyVar r)
forall (m :: * -> *) a. Freshable m a => Bool -> a -> m a
true Bool
allowTC RTypeBV Symbol Symbol RTyCon RTyVar r
t m (RTypeBV Symbol Symbol RTyCon RTyVar r
   -> r -> RTypeBV Symbol Symbol RTyCon RTyVar r)
-> m (RTypeBV Symbol Symbol RTyCon RTyVar r)
-> m (r -> RTypeBV Symbol Symbol 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
-> RTypeBV Symbol Symbol RTyCon RTyVar r
-> m (RTypeBV Symbol Symbol RTyCon RTyVar r)
forall (m :: * -> *) a. Freshable m a => Bool -> a -> m a
true Bool
allowTC RTypeBV Symbol Symbol RTyCon RTyVar r
t' m (r -> RTypeBV Symbol Symbol RTyCon RTyVar r)
-> m r -> m (RTypeBV Symbol Symbol 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 r. IsReft r => r
trueReft

trueRefType Bool
allowTC (RVar RTyVar
a r
r)
  = RTyVar -> r -> RTypeBV Symbol Symbol RTyCon RTyVar r
forall b v c tv r. tv -> r -> RTypeBV b v c tv r
RVar RTyVar
a (r -> RTypeBV Symbol Symbol RTyCon RTyVar r)
-> m r -> m (RTypeBV Symbol Symbol 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 RTypeBV Symbol Symbol RTyCon RTyVar r
ty RTypeBV Symbol Symbol RTyCon RTyVar r
tx)
  = do y'  <- m Symbol
forall (m :: * -> *) a. Freshable m a => m a
fresh
       ty' <- true allowTC ty
       tx' <- true allowTC tx
       return $ RAllE y' ty' (tx' `F.subst1` (y, F.EVar y'))

trueRefType Bool
allowTC (RRTy [(Symbol, RTypeBV Symbol Symbol RTyCon RTyVar r)]
e r
o Oblig
r RTypeBV Symbol Symbol RTyCon RTyVar r
t)
  = [(Symbol, RTypeBV Symbol Symbol RTyCon RTyVar r)]
-> r
-> Oblig
-> RTypeBV Symbol Symbol RTyCon RTyVar r
-> RTypeBV Symbol Symbol RTyCon RTyVar r
forall b v c tv r.
[(b, RTypeBV b v c tv r)]
-> r -> Oblig -> RTypeBV b v c tv r -> RTypeBV b v c tv r
RRTy [(Symbol, RTypeBV Symbol Symbol RTyCon RTyVar r)]
e r
o Oblig
r (RTypeBV Symbol Symbol RTyCon RTyVar r
 -> RTypeBV Symbol Symbol RTyCon RTyVar r)
-> m (RTypeBV Symbol Symbol RTyCon RTyVar r)
-> m (RTypeBV Symbol Symbol RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool
-> RTypeBV Symbol Symbol RTyCon RTyVar r
-> m (RTypeBV Symbol Symbol RTyCon RTyVar r)
forall (m :: * -> *) r.
(Freshable m Integer, Freshable m r, IsReft r, Subable r,
 Variable r ~ Symbol, ReftBind r ~ Symbol, ReftVar r ~ Symbol) =>
Bool -> RRType r -> m (RRType r)
trueRefType Bool
allowTC RTypeBV Symbol Symbol RTyCon RTyVar r
t

trueRefType Bool
allowTC (REx Symbol
_ RTypeBV Symbol Symbol RTyCon RTyVar r
t RTypeBV Symbol Symbol RTyCon RTyVar r
t')
  = Symbol
-> RTypeBV Symbol Symbol RTyCon RTyVar r
-> RTypeBV Symbol Symbol RTyCon RTyVar r
-> RTypeBV Symbol Symbol RTyCon RTyVar r
forall b v c tv r.
b -> RTypeBV b v c tv r -> RTypeBV b v c tv r -> RTypeBV b v c tv r
REx (Symbol
 -> RTypeBV Symbol Symbol RTyCon RTyVar r
 -> RTypeBV Symbol Symbol RTyCon RTyVar r
 -> RTypeBV Symbol Symbol RTyCon RTyVar r)
-> m Symbol
-> m (RTypeBV Symbol Symbol RTyCon RTyVar r
      -> RTypeBV Symbol Symbol RTyCon RTyVar r
      -> RTypeBV Symbol Symbol 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 (RTypeBV Symbol Symbol RTyCon RTyVar r
   -> RTypeBV Symbol Symbol RTyCon RTyVar r
   -> RTypeBV Symbol Symbol RTyCon RTyVar r)
-> m (RTypeBV Symbol Symbol RTyCon RTyVar r)
-> m (RTypeBV Symbol Symbol RTyCon RTyVar r
      -> RTypeBV Symbol Symbol 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
-> RTypeBV Symbol Symbol RTyCon RTyVar r
-> m (RTypeBV Symbol Symbol RTyCon RTyVar r)
forall (m :: * -> *) a. Freshable m a => Bool -> a -> m a
true Bool
allowTC RTypeBV Symbol Symbol RTyCon RTyVar r
t m (RTypeBV Symbol Symbol RTyCon RTyVar r
   -> RTypeBV Symbol Symbol RTyCon RTyVar r)
-> m (RTypeBV Symbol Symbol RTyCon RTyVar r)
-> m (RTypeBV Symbol Symbol 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
-> RTypeBV Symbol Symbol RTyCon RTyVar r
-> m (RTypeBV Symbol Symbol RTyCon RTyVar r)
forall (m :: * -> *) a. Freshable m a => Bool -> a -> m a
true Bool
allowTC RTypeBV Symbol Symbol RTyCon RTyVar r
t'

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

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

trueRef :: (Freshable f Integer, Freshable f r, IsReft r, F.Subable r, F.Variable r ~ F.Symbol, ReftBind r ~ F.Symbol, ReftVar r ~ F.Symbol)
        => Bool -> Ref τ (RType RTyCon RTyVar r) -> f (Ref τ (RRType r))
trueRef :: forall (f :: * -> *) r τ.
(Freshable f Integer, Freshable f r, IsReft r, Subable r,
 Variable r ~ Symbol, ReftBind r ~ Symbol, ReftVar r ~ Symbol) =>
Bool
-> Ref τ (RType RTyCon RTyVar r)
-> f (Ref τ (RType RTyCon RTyVar r))
trueRef Bool
_ (RProp [(Symbol, τ)]
_ (RHole r
_)) = Maybe SrcSpan
-> String -> f (RefB Symbol τ (RType RTyCon RTyVar r))
forall a. HasCallStack => 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 -> RefB Symbol τ (RType RTyCon RTyVar r)
forall b τ t. [(b, τ)] -> t -> RefB b τ t
RProp [(Symbol, τ)]
s (RType RTyCon RTyVar r -> RefB Symbol τ (RType RTyCon RTyVar r))
-> f (RType RTyCon RTyVar r)
-> f (RefB Symbol τ (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, IsReft r, Subable r,
 Variable r ~ Symbol, ReftBind r ~ Symbol, ReftVar r ~ Symbol) =>
Bool -> RRType r -> m (RRType r)
trueRefType Bool
allowTC RType RTyCon RTyVar r
t


-----------------------------------------------------------------------------------------------
refreshRefType :: (Freshable m Integer, Freshable m r, IsReft r, F.Subable r, F.Variable r ~ F.Symbol, ReftBind r ~ F.Symbol, ReftVar r ~ F.Symbol) => Bool -> RRType r -> m (RRType r)
-----------------------------------------------------------------------------------------------
refreshRefType :: forall (m :: * -> *) r.
(Freshable m Integer, Freshable m r, IsReft r, Subable r,
 Variable r ~ Symbol, ReftBind r ~ Symbol, ReftVar r ~ Symbol) =>
Bool -> RRType r -> m (RRType r)
refreshRefType Bool
allowTC (RAllT RTVUBV Symbol Symbol RTyCon RTyVar
α RTypeBV Symbol Symbol RTyCon RTyVar r
t r
r)
  = RTVUBV Symbol Symbol RTyCon RTyVar
-> RTypeBV Symbol Symbol RTyCon RTyVar r
-> r
-> RTypeBV Symbol Symbol RTyCon RTyVar r
forall b v c tv r.
RTVUBV b v c tv -> RTypeBV b v c tv r -> r -> RTypeBV b v c tv r
RAllT RTVUBV Symbol Symbol RTyCon RTyVar
α (RTypeBV Symbol Symbol RTyCon RTyVar r
 -> r -> RTypeBV Symbol Symbol RTyCon RTyVar r)
-> m (RTypeBV Symbol Symbol RTyCon RTyVar r)
-> m (r -> RTypeBV Symbol Symbol RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool
-> RTypeBV Symbol Symbol RTyCon RTyVar r
-> m (RTypeBV Symbol Symbol RTyCon RTyVar r)
forall (m :: * -> *) a. Freshable m a => Bool -> a -> m a
refresh Bool
allowTC RTypeBV Symbol Symbol RTyCon RTyVar r
t m (r -> RTypeBV Symbol Symbol RTyCon RTyVar r)
-> m r -> m (RTypeBV Symbol Symbol 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 PVUBV Symbol Symbol RTyCon RTyVar
π RTypeBV Symbol Symbol RTyCon RTyVar r
t)
  = PVUBV Symbol Symbol RTyCon RTyVar
-> RTypeBV Symbol Symbol RTyCon RTyVar r
-> RTypeBV Symbol Symbol RTyCon RTyVar r
forall b v c tv r.
PVUBV b v c tv -> RTypeBV b v c tv r -> RTypeBV b v c tv r
RAllP PVUBV Symbol Symbol RTyCon RTyVar
π (RTypeBV Symbol Symbol RTyCon RTyVar r
 -> RTypeBV Symbol Symbol RTyCon RTyVar r)
-> m (RTypeBV Symbol Symbol RTyCon RTyVar r)
-> m (RTypeBV Symbol Symbol RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool
-> RTypeBV Symbol Symbol RTyCon RTyVar r
-> m (RTypeBV Symbol Symbol RTyCon RTyVar r)
forall (m :: * -> *) a. Freshable m a => Bool -> a -> m a
refresh Bool
allowTC RTypeBV Symbol Symbol RTyCon RTyVar r
t

refreshRefType Bool
allowTC (RFun Symbol
sym RFInfo
i RTypeBV Symbol Symbol RTyCon RTyVar r
t RTypeBV Symbol Symbol RTyCon RTyVar r
t' r
_)
  | Symbol
sym Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
F.dummySymbol = (\Symbol
b RTypeBV Symbol Symbol RTyCon RTyVar r
t1 RTypeBV Symbol Symbol RTyCon RTyVar r
t2 -> Symbol
-> RFInfo
-> RTypeBV Symbol Symbol RTyCon RTyVar r
-> RTypeBV Symbol Symbol RTyCon RTyVar r
-> r
-> RTypeBV Symbol Symbol RTyCon RTyVar r
forall b v c tv r.
b
-> RFInfo
-> RTypeBV b v c tv r
-> RTypeBV b v c tv r
-> r
-> RTypeBV b v c tv r
RFun Symbol
b RFInfo
i RTypeBV Symbol Symbol RTyCon RTyVar r
t1 RTypeBV Symbol Symbol RTyCon RTyVar r
t2 r
forall r. IsReft r => r
trueReft) (Symbol
 -> RTypeBV Symbol Symbol RTyCon RTyVar r
 -> RTypeBV Symbol Symbol RTyCon RTyVar r
 -> RTypeBV Symbol Symbol RTyCon RTyVar r)
-> m Symbol
-> m (RTypeBV Symbol Symbol RTyCon RTyVar r
      -> RTypeBV Symbol Symbol RTyCon RTyVar r
      -> RTypeBV Symbol Symbol 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 (RTypeBV Symbol Symbol RTyCon RTyVar r
   -> RTypeBV Symbol Symbol RTyCon RTyVar r
   -> RTypeBV Symbol Symbol RTyCon RTyVar r)
-> m (RTypeBV Symbol Symbol RTyCon RTyVar r)
-> m (RTypeBV Symbol Symbol RTyCon RTyVar r
      -> RTypeBV Symbol Symbol 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
-> RTypeBV Symbol Symbol RTyCon RTyVar r
-> m (RTypeBV Symbol Symbol RTyCon RTyVar r)
forall (m :: * -> *) a. Freshable m a => Bool -> a -> m a
refresh Bool
allowTC RTypeBV Symbol Symbol RTyCon RTyVar r
t m (RTypeBV Symbol Symbol RTyCon RTyVar r
   -> RTypeBV Symbol Symbol RTyCon RTyVar r)
-> m (RTypeBV Symbol Symbol RTyCon RTyVar r)
-> m (RTypeBV Symbol Symbol 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
-> RTypeBV Symbol Symbol RTyCon RTyVar r
-> m (RTypeBV Symbol Symbol RTyCon RTyVar r)
forall (m :: * -> *) a. Freshable m a => Bool -> a -> m a
refresh Bool
allowTC RTypeBV Symbol Symbol RTyCon RTyVar r
t'
  | Bool
otherwise          = (\RTypeBV Symbol Symbol RTyCon RTyVar r
t1 RTypeBV Symbol Symbol RTyCon RTyVar r
t2 -> Symbol
-> RFInfo
-> RTypeBV Symbol Symbol RTyCon RTyVar r
-> RTypeBV Symbol Symbol RTyCon RTyVar r
-> r
-> RTypeBV Symbol Symbol RTyCon RTyVar r
forall b v c tv r.
b
-> RFInfo
-> RTypeBV b v c tv r
-> RTypeBV b v c tv r
-> r
-> RTypeBV b v c tv r
RFun Symbol
sym RFInfo
i RTypeBV Symbol Symbol RTyCon RTyVar r
t1 RTypeBV Symbol Symbol RTyCon RTyVar r
t2 r
forall r. IsReft r => r
trueReft)   (RTypeBV Symbol Symbol RTyCon RTyVar r
 -> RTypeBV Symbol Symbol RTyCon RTyVar r
 -> RTypeBV Symbol Symbol RTyCon RTyVar r)
-> m (RTypeBV Symbol Symbol RTyCon RTyVar r)
-> m (RTypeBV Symbol Symbol RTyCon RTyVar r
      -> RTypeBV Symbol Symbol RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool
-> RTypeBV Symbol Symbol RTyCon RTyVar r
-> m (RTypeBV Symbol Symbol RTyCon RTyVar r)
forall (m :: * -> *) a. Freshable m a => Bool -> a -> m a
refresh Bool
allowTC RTypeBV Symbol Symbol RTyCon RTyVar r
t m (RTypeBV Symbol Symbol RTyCon RTyVar r
   -> RTypeBV Symbol Symbol RTyCon RTyVar r)
-> m (RTypeBV Symbol Symbol RTyCon RTyVar r)
-> m (RTypeBV Symbol Symbol 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
-> RTypeBV Symbol Symbol RTyCon RTyVar r
-> m (RTypeBV Symbol Symbol RTyCon RTyVar r)
forall (m :: * -> *) a. Freshable m a => Bool -> a -> m a
refresh Bool
allowTC RTypeBV Symbol Symbol RTyCon RTyVar r
t'

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

refreshRefType Bool
allowTC (RApp RTyCon
rc [RTypeBV Symbol Symbol RTyCon RTyVar r]
ts [RTPropBV Symbol Symbol RTyCon RTyVar r]
rs r
r)
  = RTyCon
-> [RTypeBV Symbol Symbol RTyCon RTyVar r]
-> [RTPropBV Symbol Symbol RTyCon RTyVar r]
-> r
-> RTypeBV Symbol Symbol RTyCon RTyVar r
forall b v c tv r.
c
-> [RTypeBV b v c tv r]
-> [RTPropBV b v c tv r]
-> r
-> RTypeBV b v c tv r
RApp RTyCon
rc ([RTypeBV Symbol Symbol RTyCon RTyVar r]
 -> [RTPropBV Symbol Symbol RTyCon RTyVar r]
 -> r
 -> RTypeBV Symbol Symbol RTyCon RTyVar r)
-> m [RTypeBV Symbol Symbol RTyCon RTyVar r]
-> m ([RTPropBV Symbol Symbol RTyCon RTyVar r]
      -> r -> RTypeBV Symbol Symbol RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (RTypeBV Symbol Symbol RTyCon RTyVar r
 -> m (RTypeBV Symbol Symbol RTyCon RTyVar r))
-> [RTypeBV Symbol Symbol RTyCon RTyVar r]
-> m [RTypeBV Symbol Symbol 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
-> RTypeBV Symbol Symbol RTyCon RTyVar r
-> m (RTypeBV Symbol Symbol RTyCon RTyVar r)
forall (m :: * -> *) a. Freshable m a => Bool -> a -> m a
refresh Bool
allowTC) [RTypeBV Symbol Symbol RTyCon RTyVar r]
ts m ([RTPropBV Symbol Symbol RTyCon RTyVar r]
   -> r -> RTypeBV Symbol Symbol RTyCon RTyVar r)
-> m [RTPropBV Symbol Symbol RTyCon RTyVar r]
-> m (r -> RTypeBV Symbol Symbol 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
<*> (RTPropBV Symbol Symbol RTyCon RTyVar r
 -> m (RTPropBV Symbol Symbol RTyCon RTyVar r))
-> [RTPropBV Symbol Symbol RTyCon RTyVar r]
-> m [RTPropBV Symbol Symbol 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
-> RTPropBV Symbol Symbol RTyCon RTyVar r
-> m (RTPropBV Symbol Symbol RTyCon RTyVar r)
forall (f :: * -> *) r τ.
(Freshable f Integer, Freshable f r, IsReft r, Subable r,
 Variable r ~ Symbol, ReftBind r ~ Symbol, ReftVar r ~ Symbol) =>
Bool
-> Ref τ (RType RTyCon RTyVar r)
-> f (Ref τ (RType RTyCon RTyVar r))
refreshRef Bool
allowTC) [RTPropBV Symbol Symbol RTyCon RTyVar r]
rs m (r -> RTypeBV Symbol Symbol RTyCon RTyVar r)
-> m r -> m (RTypeBV Symbol Symbol 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 -> RTypeBV Symbol Symbol RTyCon RTyVar r
forall b v c tv r. tv -> r -> RTypeBV b v c tv r
RVar RTyVar
a (r -> RTypeBV Symbol Symbol RTyCon RTyVar r)
-> m r -> m (RTypeBV Symbol Symbol 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 RTypeBV Symbol Symbol RTyCon RTyVar r
t RTypeBV Symbol Symbol RTyCon RTyVar r
t' r
r)
  = RTypeBV Symbol Symbol RTyCon RTyVar r
-> RTypeBV Symbol Symbol RTyCon RTyVar r
-> r
-> RTypeBV Symbol Symbol RTyCon RTyVar r
forall b v c tv r.
RTypeBV b v c tv r -> RTypeBV b v c tv r -> r -> RTypeBV b v c tv r
RAppTy (RTypeBV Symbol Symbol RTyCon RTyVar r
 -> RTypeBV Symbol Symbol RTyCon RTyVar r
 -> r
 -> RTypeBV Symbol Symbol RTyCon RTyVar r)
-> m (RTypeBV Symbol Symbol RTyCon RTyVar r)
-> m (RTypeBV Symbol Symbol RTyCon RTyVar r
      -> r -> RTypeBV Symbol Symbol RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool
-> RTypeBV Symbol Symbol RTyCon RTyVar r
-> m (RTypeBV Symbol Symbol RTyCon RTyVar r)
forall (m :: * -> *) a. Freshable m a => Bool -> a -> m a
refresh Bool
allowTC RTypeBV Symbol Symbol RTyCon RTyVar r
t m (RTypeBV Symbol Symbol RTyCon RTyVar r
   -> r -> RTypeBV Symbol Symbol RTyCon RTyVar r)
-> m (RTypeBV Symbol Symbol RTyCon RTyVar r)
-> m (r -> RTypeBV Symbol Symbol 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
-> RTypeBV Symbol Symbol RTyCon RTyVar r
-> m (RTypeBV Symbol Symbol RTyCon RTyVar r)
forall (m :: * -> *) a. Freshable m a => Bool -> a -> m a
refresh Bool
allowTC RTypeBV Symbol Symbol RTyCon RTyVar r
t' m (r -> RTypeBV Symbol Symbol RTyCon RTyVar r)
-> m r -> m (RTypeBV Symbol Symbol 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 RTypeBV Symbol Symbol RTyCon RTyVar r
ty RTypeBV Symbol Symbol RTyCon RTyVar r
tx)
  = do y'  <- m Symbol
forall (m :: * -> *) a. Freshable m a => m a
fresh
       ty' <- refresh allowTC ty
       tx' <- refresh allowTC tx
       return $ RAllE y' ty' (tx' `F.subst1` (y, F.EVar y'))

refreshRefType Bool
allowTC (RRTy [(Symbol, RTypeBV Symbol Symbol RTyCon RTyVar r)]
e r
o Oblig
r RTypeBV Symbol Symbol RTyCon RTyVar r
t)
  = [(Symbol, RTypeBV Symbol Symbol RTyCon RTyVar r)]
-> r
-> Oblig
-> RTypeBV Symbol Symbol RTyCon RTyVar r
-> RTypeBV Symbol Symbol RTyCon RTyVar r
forall b v c tv r.
[(b, RTypeBV b v c tv r)]
-> r -> Oblig -> RTypeBV b v c tv r -> RTypeBV b v c tv r
RRTy [(Symbol, RTypeBV Symbol Symbol RTyCon RTyVar r)]
e r
o Oblig
r (RTypeBV Symbol Symbol RTyCon RTyVar r
 -> RTypeBV Symbol Symbol RTyCon RTyVar r)
-> m (RTypeBV Symbol Symbol RTyCon RTyVar r)
-> m (RTypeBV Symbol Symbol RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool
-> RTypeBV Symbol Symbol RTyCon RTyVar r
-> m (RTypeBV Symbol Symbol RTyCon RTyVar r)
forall (m :: * -> *) r.
(Freshable m Integer, Freshable m r, IsReft r, Subable r,
 Variable r ~ Symbol, ReftBind r ~ Symbol, ReftVar r ~ Symbol) =>
Bool -> RRType r -> m (RRType r)
refreshRefType Bool
allowTC RTypeBV Symbol Symbol RTyCon RTyVar r
t

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

refreshRef :: (Freshable f Integer, Freshable f r, IsReft r, F.Subable r, F.Variable r ~ F.Symbol, ReftBind r ~ F.Symbol, ReftVar r ~ F.Symbol)
           => Bool -> Ref τ (RType RTyCon RTyVar r) -> f (Ref τ (RRType r))
refreshRef :: forall (f :: * -> *) r τ.
(Freshable f Integer, Freshable f r, IsReft r, Subable r,
 Variable r ~ Symbol, ReftBind r ~ Symbol, ReftVar r ~ Symbol) =>
Bool
-> Ref τ (RType RTyCon RTyVar r)
-> f (Ref τ (RType RTyCon RTyVar r))
refreshRef Bool
_ (RProp [(Symbol, τ)]
_ (RHole r
_)) = Maybe SrcSpan
-> String -> f (RefB Symbol τ (RType RTyCon RTyVar r))
forall a. HasCallStack => 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 -> RefB Symbol τ (RType RTyCon RTyVar r)
forall b τ t. [(b, τ)] -> t -> RefB b τ t
RProp ([(Symbol, τ)]
 -> RType RTyCon RTyVar r -> RefB Symbol τ (RType RTyCon RTyVar r))
-> f [(Symbol, τ)]
-> f (RType RTyCon RTyVar r
      -> RefB Symbol τ (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 -> RefB Symbol τ (RType RTyCon RTyVar r))
-> f (RType RTyCon RTyVar r)
-> f (RefB Symbol τ (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, IsReft r, Subable r,
 Variable r ~ Symbol, ReftBind r ~ Symbol, ReftVar r ~ Symbol) =>
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 RTVUBV Symbol Symbol RTyCon RTyVar
a SpecType
t RReft
r) =
  RTVUBV Symbol Symbol RTyCon RTyVar -> SpecType -> RReft -> SpecType
forall b v c tv r.
RTVUBV b v c tv -> RTypeBV b v c tv r -> r -> RTypeBV b v c tv r
RAllT RTVUBV Symbol Symbol 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 PVUBV Symbol Symbol RTyCon RTyVar
p SpecType
t) =
  PVUBV Symbol Symbol RTyCon RTyVar -> SpecType -> SpecType
forall b v c tv r.
PVUBV b v c tv -> RTypeBV b v c tv r -> RTypeBV b v c tv r
RAllP PVUBV Symbol Symbol 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
  t1' <- SpecType -> m SpecType
forall (m :: * -> *). FreshM m => SpecType -> m SpecType
refreshVV SpecType
t1
  t2' <- refreshVV t2
  shiftVV (REx x t1' t2') <$> fresh

refreshVV (RFun Symbol
x RFInfo
i SpecType
t1 SpecType
t2 RReft
r) = do
  t1' <- SpecType -> m SpecType
forall (m :: * -> *). FreshM m => SpecType -> m SpecType
refreshVV SpecType
t1
  t2' <- refreshVV t2
  shiftVV (RFun x i t1' t2' r) <$> fresh

refreshVV (RAppTy SpecType
t1 SpecType
t2 RReft
r) = do
  t1' <- SpecType -> m SpecType
forall (m :: * -> *). FreshM m => SpecType -> m SpecType
refreshVV SpecType
t1
  t2' <- refreshVV t2
  shiftVV (RAppTy t1' t2' r) <$> fresh

refreshVV (RApp RTyCon
c [SpecType]
ts [RTPropBV Symbol Symbol RTyCon RTyVar RReft]
rs RReft
r) = do
  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
  rs' <- mapM refreshVVRef rs
  shiftVV (RApp c ts' rs' r) <$> fresh

refreshVV SpecType
t =
  SpecType -> Symbol -> SpecType
forall c (f :: * -> *) tv.
(TyConable c, IsReft (f Reft), Functor f, Subable (f Reft),
 Variable (f Reft) ~ Variable Reft,
 ReftBind (f Reft) ~ ReftBind Reft) =>
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))
  = RefB Symbol b SpecType -> m (RefB Symbol b SpecType)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (RefB Symbol b SpecType -> m (RefB Symbol b SpecType))
-> RefB Symbol b SpecType -> m (RefB Symbol b SpecType)
forall a b. (a -> b) -> a -> b
$ [(Symbol, b)] -> SpecType -> RefB Symbol b SpecType
forall b τ t. [(b, τ)] -> t -> RefB b τ t
RProp [(Symbol, b)]
ss (RReft -> SpecType
forall b v c tv r. r -> RTypeBV b v c tv r
RHole RReft
r)

refreshVVRef (RProp [(Symbol, b)]
ss SpecType
t)
  = do 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 = [(Symbol, Expr)] -> SubstV Symbol
forall v. Hashable v => [(v, ExprBV v v)] -> SubstV v
F.mkSubst ([(Symbol, Expr)] -> SubstV Symbol)
-> [(Symbol, Expr)] -> SubstV Symbol
forall a b. (a -> b) -> a -> b
$ [Symbol] -> [Expr] -> [(Symbol, Expr)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
syms (Symbol -> Expr
forall b v. v -> ExprBV b v
F.EVar (Symbol -> Expr) -> [Symbol] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
xs)
       t'    <- refreshVV t
       return $ RProp (zip xs bs) (F.subst su 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, SubstV Symbol) -> SpecType
forall a b. (a, b) -> a
fst ((SpecType, SubstV Symbol) -> SpecType)
-> m (SpecType, SubstV Symbol) -> m SpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SpecType -> m (SpecType, SubstV Symbol)
forall (m :: * -> *).
FreshM m =>
SpecType -> m (SpecType, SubstV Symbol)
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, SubstV Symbol)
refreshArgsSub SpecType
t
  = do 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
       xs'    <- mapM (const fresh) xs
       let sus = [(Symbol, Expr)] -> SubstV Symbol
forall v. Hashable v => [(v, ExprBV v v)] -> SubstV v
F.mkSubst ([(Symbol, Expr)] -> SubstV Symbol)
-> [[(Symbol, Expr)]] -> [SubstV Symbol]
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
forall b v. v -> ExprBV b v
F.EVar (Symbol -> Expr) -> [Symbol] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
xs'))
       let su  = [SubstV Symbol] -> SubstV Symbol
forall a. HasCallStack => [a] -> a
last [SubstV Symbol]
sus
       ts'    <- mapM refreshPs $ zipWith F.subst sus ts
       let rs' = (SubstV Symbol -> RReft -> RReft)
-> [SubstV Symbol] -> [RReft] -> [RReft]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith SubstV Symbol -> RReft -> RReft
SubstV (Variable RReft) -> RReft -> RReft
forall a.
(Subable a, HasCallStack) =>
SubstV (Variable a) -> a -> a
F.subst [SubstV Symbol]
sus [RReft]
rs
       tr     <- refreshPs $ F.subst su tbd
       let t'  = RTypeRepBV Symbol Symbol RTyCon RTyVar RReft -> SpecType
forall b v c tv r. RTypeRepBV b v c tv r -> RTypeBV b v c tv r
fromRTypeRep (RTypeRepBV Symbol Symbol RTyCon RTyVar RReft -> SpecType)
-> RTypeRepBV Symbol Symbol RTyCon RTyVar RReft -> SpecType
forall a b. (a -> b) -> a -> b
$ RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
trep {ty_binds = xs', ty_args = ts', ty_res = tr, ty_refts = rs'}
       return (t', su)
    where
       trep :: RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
trep    = SpecType -> RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
forall b v c tv r. RTypeBV b v c tv r -> RTypeRepBV b v c tv r
toRTypeRep SpecType
t
       xs :: [Symbol]
xs      = RTypeRepBV Symbol Symbol RTyCon RTyVar RReft -> [Symbol]
forall b v c tv r. RTypeRepBV b v c tv r -> [b]
ty_binds RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
trep
       ts_u :: [SpecType]
ts_u    = RTypeRepBV Symbol Symbol RTyCon RTyVar RReft -> [SpecType]
forall b v c tv r. RTypeRepBV b v c tv r -> [RTypeBV b v c tv r]
ty_args  RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
trep
       tbd :: SpecType
tbd     = RTypeRepBV Symbol Symbol RTyCon RTyVar RReft -> SpecType
forall b v c tv r. RTypeRepBV b v c tv r -> RTypeBV b v c tv r
ty_res   RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
trep
       rs :: [RReft]
rs      = RTypeRepBV Symbol Symbol RTyCon RTyVar RReft -> [RReft]
forall b v c tv r. RTypeRepBV b v c tv r -> [r]
ty_refts RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
trep

refreshPs :: (FreshM m) => SpecType -> m SpecType
refreshPs :: forall (m :: * -> *). FreshM m => SpecType -> m SpecType
refreshPs = (RTPropBV Symbol Symbol RTyCon RTyVar RReft
 -> m (RTPropBV Symbol Symbol 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 RTPropBV Symbol Symbol RTyCon RTyVar RReft
-> m (RTPropBV Symbol Symbol RTyCon RTyVar RReft)
forall (m :: * -> *) b.
Freshable m Integer =>
Ref b SpecType -> m (Ref b SpecType)
go
  where
    go :: RefB Symbol τ SpecType -> m (RefB Symbol τ SpecType)
go (RProp [(Symbol, τ)]
s SpecType
st) = do
      t'    <- SpecType -> m SpecType
forall (m :: * -> *). FreshM m => SpecType -> m SpecType
refreshPs SpecType
st
      xs    <- mapM (const fresh) s
      let su = [(Symbol, Expr)] -> SubstV Symbol
forall v. Hashable v => [(v, ExprBV v v)] -> SubstV v
F.mkSubst [(Symbol
y, Symbol -> Expr
forall b v. v -> ExprBV b v
F.EVar Symbol
x) | (Symbol
x, (Symbol
y, τ
_)) <- [Symbol] -> [(Symbol, τ)] -> [(Symbol, (Symbol, τ))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
xs [(Symbol, τ)]
s]
      return $ RProp [(x, t) | (x, (_, t)) <- zip xs s] $ F.subst su t'

--------------------------------------------------------------------------------
refreshHoles :: (F.Symbolic t, IsReft r, ReftBind r ~ F.Symbol, ReftVar r ~ F.Symbol, 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, IsReft r, ReftBind r ~ Symbol, ReftVar r ~ Symbol,
 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, IsReft r, ReftBind r ~ Symbol, ReftVar r ~ Symbol,
 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, IsReft r, ReftBind r ~ F.Symbol, ReftVar r ~ F.Symbol, 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, IsReft r, ReftBind r ~ Symbol, ReftVar r ~ Symbol,
 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.
(IsReft r, ReftBind r ~ Symbol, ReftVar r ~ Symbol, 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 :: * -> *}.
(ReftBind a ~ Symbol, ReftVar a ~ Symbol, ToReft 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.
(ToReft r, ReftBind r ~ Symbol, ReftVar r ~ Symbol) =>
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 :: (IsReft r, ReftBind r ~ F.Symbol, ReftVar r ~ F.Symbol, TyConable c) => RType c tv r -> Bool
noHoles :: forall r c tv.
(IsReft r, ReftBind r ~ Symbol, ReftVar r ~ Symbol, TyConable c) =>
RType c tv r -> Bool
noHoles = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ([Bool] -> Bool)
-> (RTypeBV Symbol Symbol c tv r -> [Bool])
-> RTypeBV Symbol Symbol c tv r
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool
-> (SEnvB Symbol (RTypeBV Symbol Symbol c tv r)
    -> r -> [Bool] -> [Bool])
-> [Bool]
-> RTypeBV Symbol Symbol c tv r
-> [Bool]
forall r c b v tv z.
(IsReft r, TyConable c, Binder b, ReftBind r ~ b) =>
Bool
-> (SEnvB b (RTypeBV b v c tv r) -> r -> z -> z)
-> z
-> RTypeBV b v c tv r
-> z
foldReft Bool
False (\SEnvB Symbol (RTypeBV Symbol Symbol c tv r)
_ r
r [Bool]
bs -> Bool -> Bool
not (r -> Bool
forall r.
(ToReft r, ReftBind r ~ Symbol, ReftVar r ~ Symbol) =>
r -> Bool
hasHole r
r) Bool -> [Bool] -> [Bool]
forall a. a -> [a] -> [a]
: [Bool]
bs) []