{-# 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.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
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 -> SubstV Symbol -> Expr
forall v. KVar -> SubstV v -> ExprV v
`F.PKVar` SubstV Symbol
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. 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 v. (Symbol, ExprV v) -> ReftV v
F.Reft (Symbol
v, Expr
forall v. ExprV v
F.PTrue)
  refresh :: Bool -> Reft -> m Reft
refresh Bool
_ (F.Reft (Symbol
_,Expr
_)) = ((Symbol, Expr) -> Reft
forall v. (Symbol, ExprV v) -> ReftV 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 PredicateV Symbol
_)    = Reft -> PredicateV Symbol -> RReft
forall v r. r -> PredicateV v -> UReftV v r
MkUReft (Reft -> PredicateV Symbol -> RReft)
-> m Reft -> m (PredicateV 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 (PredicateV Symbol -> RReft) -> m (PredicateV 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
<*> PredicateV Symbol -> m (PredicateV Symbol)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return PredicateV Symbol
forall a. Monoid a => a
mempty
  refresh :: Bool -> RReft -> m RReft
refresh Bool
allowTC (MkUReft Reft
r PredicateV Symbol
_) = Reft -> PredicateV Symbol -> RReft
forall v r. r -> PredicateV v -> UReftV v r
MkUReft (Reft -> PredicateV Symbol -> RReft)
-> m Reft -> m (PredicateV 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 (PredicateV Symbol -> RReft) -> m (PredicateV 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
<*> PredicateV Symbol -> m (PredicateV Symbol)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return PredicateV Symbol
forall a. Monoid a => a
mempty

instance (Freshable m Integer, Freshable m r, Reftable r ) => 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, 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, 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 RTVUV Symbol RTyCon RTyVar
α RTypeV Symbol RTyCon RTyVar r
t r
r)
  = RTVUV Symbol RTyCon RTyVar
-> RTypeV Symbol RTyCon RTyVar r
-> r
-> RTypeV Symbol RTyCon RTyVar r
forall v c tv r.
RTVUV v c tv -> RTypeV v c tv r -> r -> RTypeV v c tv r
RAllT RTVUV Symbol RTyCon RTyVar
α (RTypeV Symbol RTyCon RTyVar r
 -> r -> RTypeV Symbol RTyCon RTyVar r)
-> m (RTypeV Symbol RTyCon RTyVar r)
-> m (r -> RTypeV Symbol RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool
-> RTypeV Symbol RTyCon RTyVar r
-> m (RTypeV Symbol RTyCon RTyVar r)
forall (m :: * -> *) a. Freshable m a => Bool -> a -> m a
true Bool
allowTC RTypeV Symbol RTyCon RTyVar r
t m (r -> RTypeV Symbol RTyCon RTyVar r)
-> m r -> m (RTypeV 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 PVUV Symbol RTyCon RTyVar
π RTypeV Symbol RTyCon RTyVar r
t)
  = PVUV Symbol RTyCon RTyVar
-> RTypeV Symbol RTyCon RTyVar r -> RTypeV Symbol RTyCon RTyVar r
forall v c tv r. PVUV v c tv -> RTypeV v c tv r -> RTypeV v c tv r
RAllP PVUV Symbol RTyCon RTyVar
π (RTypeV Symbol RTyCon RTyVar r -> RTypeV Symbol RTyCon RTyVar r)
-> m (RTypeV Symbol RTyCon RTyVar r)
-> m (RTypeV Symbol RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool
-> RTypeV Symbol RTyCon RTyVar r
-> m (RTypeV Symbol RTyCon RTyVar r)
forall (m :: * -> *) a. Freshable m a => Bool -> a -> m a
true Bool
allowTC RTypeV Symbol RTyCon RTyVar r
t

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

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

trueRefType Bool
allowTC (RApp RTyCon
c [RTypeV Symbol RTyCon RTyVar r]
ts [RTPropV Symbol RTyCon RTyVar r]
rs r
r)
  = RTyCon
-> [RTypeV Symbol RTyCon RTyVar r]
-> [RTPropV Symbol RTyCon RTyVar r]
-> r
-> RTypeV Symbol RTyCon RTyVar r
forall v c tv r.
c
-> [RTypeV v c tv r] -> [RTPropV v c tv r] -> r -> RTypeV v c tv r
RApp RTyCon
c ([RTypeV Symbol RTyCon RTyVar r]
 -> [RTPropV Symbol RTyCon RTyVar r]
 -> r
 -> RTypeV Symbol RTyCon RTyVar r)
-> m [RTypeV Symbol RTyCon RTyVar r]
-> m ([RTPropV Symbol RTyCon RTyVar r]
      -> r -> RTypeV Symbol RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (RTypeV Symbol RTyCon RTyVar r
 -> m (RTypeV Symbol RTyCon RTyVar r))
-> [RTypeV Symbol RTyCon RTyVar r]
-> m [RTypeV 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
-> RTypeV Symbol RTyCon RTyVar r
-> m (RTypeV Symbol RTyCon RTyVar r)
forall (m :: * -> *) a. Freshable m a => Bool -> a -> m a
true Bool
allowTC) [RTypeV Symbol RTyCon RTyVar r]
ts m ([RTPropV Symbol RTyCon RTyVar r]
   -> r -> RTypeV Symbol RTyCon RTyVar r)
-> m [RTPropV Symbol RTyCon RTyVar r]
-> m (r -> RTypeV 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
<*> (RTPropV Symbol RTyCon RTyVar r
 -> m (RTPropV Symbol RTyCon RTyVar r))
-> [RTPropV Symbol RTyCon RTyVar r]
-> m [RTPropV 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
-> RTPropV Symbol RTyCon RTyVar r
-> m (RTPropV Symbol 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) [RTPropV Symbol RTyCon RTyVar r]
rs m (r -> RTypeV Symbol RTyCon RTyVar r)
-> m r -> m (RTypeV 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 RTypeV Symbol RTyCon RTyVar r
t RTypeV Symbol RTyCon RTyVar r
t' r
_)
  = RTypeV Symbol RTyCon RTyVar r
-> RTypeV Symbol RTyCon RTyVar r
-> r
-> RTypeV Symbol RTyCon RTyVar r
forall v c tv r.
RTypeV v c tv r -> RTypeV v c tv r -> r -> RTypeV v c tv r
RAppTy (RTypeV Symbol RTyCon RTyVar r
 -> RTypeV Symbol RTyCon RTyVar r
 -> r
 -> RTypeV Symbol RTyCon RTyVar r)
-> m (RTypeV Symbol RTyCon RTyVar r)
-> m (RTypeV Symbol RTyCon RTyVar r
      -> r -> RTypeV Symbol RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool
-> RTypeV Symbol RTyCon RTyVar r
-> m (RTypeV Symbol RTyCon RTyVar r)
forall (m :: * -> *) a. Freshable m a => Bool -> a -> m a
true Bool
allowTC RTypeV Symbol RTyCon RTyVar r
t m (RTypeV Symbol RTyCon RTyVar r
   -> r -> RTypeV Symbol RTyCon RTyVar r)
-> m (RTypeV Symbol RTyCon RTyVar r)
-> m (r -> RTypeV 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
-> RTypeV Symbol RTyCon RTyVar r
-> m (RTypeV Symbol RTyCon RTyVar r)
forall (m :: * -> *) a. Freshable m a => Bool -> a -> m a
true Bool
allowTC RTypeV Symbol RTyCon RTyVar r
t' m (r -> RTypeV Symbol RTyCon RTyVar r)
-> m r -> m (RTypeV 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 a. Monoid a => a
mempty

trueRefType Bool
allowTC (RVar RTyVar
a r
r)
  = RTyVar -> r -> RTypeV Symbol RTyCon RTyVar r
forall v c tv r. tv -> r -> RTypeV v c tv r
RVar RTyVar
a (r -> RTypeV Symbol RTyCon RTyVar r)
-> m r -> m (RTypeV 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 RTypeV Symbol RTyCon RTyVar r
ty RTypeV 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, RTypeV Symbol RTyCon RTyVar r)]
e r
o Oblig
r RTypeV Symbol RTyCon RTyVar r
t)
  = [(Symbol, RTypeV Symbol RTyCon RTyVar r)]
-> r
-> Oblig
-> RTypeV Symbol RTyCon RTyVar r
-> RTypeV Symbol RTyCon RTyVar r
forall v c tv r.
[(Symbol, RTypeV v c tv r)]
-> r -> Oblig -> RTypeV v c tv r -> RTypeV v c tv r
RRTy [(Symbol, RTypeV Symbol RTyCon RTyVar r)]
e r
o Oblig
r (RTypeV Symbol RTyCon RTyVar r -> RTypeV Symbol RTyCon RTyVar r)
-> m (RTypeV Symbol RTyCon RTyVar r)
-> m (RTypeV Symbol RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool
-> RTypeV Symbol RTyCon RTyVar r
-> m (RTypeV Symbol RTyCon RTyVar r)
forall (m :: * -> *) r.
(Freshable m Integer, Freshable m r, Reftable r) =>
Bool -> RRType r -> m (RRType r)
trueRefType Bool
allowTC RTypeV Symbol RTyCon RTyVar r
t

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

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

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

trueRef :: (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. 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 -> 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, 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 RTVUV Symbol RTyCon RTyVar
α RTypeV Symbol RTyCon RTyVar r
t r
r)
  = RTVUV Symbol RTyCon RTyVar
-> RTypeV Symbol RTyCon RTyVar r
-> r
-> RTypeV Symbol RTyCon RTyVar r
forall v c tv r.
RTVUV v c tv -> RTypeV v c tv r -> r -> RTypeV v c tv r
RAllT RTVUV Symbol RTyCon RTyVar
α (RTypeV Symbol RTyCon RTyVar r
 -> r -> RTypeV Symbol RTyCon RTyVar r)
-> m (RTypeV Symbol RTyCon RTyVar r)
-> m (r -> RTypeV Symbol RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool
-> RTypeV Symbol RTyCon RTyVar r
-> m (RTypeV Symbol RTyCon RTyVar r)
forall (m :: * -> *) a. Freshable m a => Bool -> a -> m a
refresh Bool
allowTC RTypeV Symbol RTyCon RTyVar r
t m (r -> RTypeV Symbol RTyCon RTyVar r)
-> m r -> m (RTypeV 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 PVUV Symbol RTyCon RTyVar
π RTypeV Symbol RTyCon RTyVar r
t)
  = PVUV Symbol RTyCon RTyVar
-> RTypeV Symbol RTyCon RTyVar r -> RTypeV Symbol RTyCon RTyVar r
forall v c tv r. PVUV v c tv -> RTypeV v c tv r -> RTypeV v c tv r
RAllP PVUV Symbol RTyCon RTyVar
π (RTypeV Symbol RTyCon RTyVar r -> RTypeV Symbol RTyCon RTyVar r)
-> m (RTypeV Symbol RTyCon RTyVar r)
-> m (RTypeV Symbol RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool
-> RTypeV Symbol RTyCon RTyVar r
-> m (RTypeV Symbol RTyCon RTyVar r)
forall (m :: * -> *) a. Freshable m a => Bool -> a -> m a
refresh Bool
allowTC RTypeV Symbol RTyCon RTyVar r
t

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

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

refreshRefType Bool
allowTC (RApp RTyCon
rc [RTypeV Symbol RTyCon RTyVar r]
ts [RTPropV Symbol RTyCon RTyVar r]
rs r
r)
  = RTyCon
-> [RTypeV Symbol RTyCon RTyVar r]
-> [RTPropV Symbol RTyCon RTyVar r]
-> r
-> RTypeV Symbol RTyCon RTyVar r
forall v c tv r.
c
-> [RTypeV v c tv r] -> [RTPropV v c tv r] -> r -> RTypeV v c tv r
RApp RTyCon
rc ([RTypeV Symbol RTyCon RTyVar r]
 -> [RTPropV Symbol RTyCon RTyVar r]
 -> r
 -> RTypeV Symbol RTyCon RTyVar r)
-> m [RTypeV Symbol RTyCon RTyVar r]
-> m ([RTPropV Symbol RTyCon RTyVar r]
      -> r -> RTypeV Symbol RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (RTypeV Symbol RTyCon RTyVar r
 -> m (RTypeV Symbol RTyCon RTyVar r))
-> [RTypeV Symbol RTyCon RTyVar r]
-> m [RTypeV 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
-> RTypeV Symbol RTyCon RTyVar r
-> m (RTypeV Symbol RTyCon RTyVar r)
forall (m :: * -> *) a. Freshable m a => Bool -> a -> m a
refresh Bool
allowTC) [RTypeV Symbol RTyCon RTyVar r]
ts m ([RTPropV Symbol RTyCon RTyVar r]
   -> r -> RTypeV Symbol RTyCon RTyVar r)
-> m [RTPropV Symbol RTyCon RTyVar r]
-> m (r -> RTypeV 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
<*> (RTPropV Symbol RTyCon RTyVar r
 -> m (RTPropV Symbol RTyCon RTyVar r))
-> [RTPropV Symbol RTyCon RTyVar r]
-> m [RTPropV 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
-> RTPropV Symbol RTyCon RTyVar r
-> m (RTPropV Symbol 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) [RTPropV Symbol RTyCon RTyVar r]
rs m (r -> RTypeV Symbol RTyCon RTyVar r)
-> m r -> m (RTypeV 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 -> RTypeV Symbol RTyCon RTyVar r
forall v c tv r. tv -> r -> RTypeV v c tv r
RVar RTyVar
a (r -> RTypeV Symbol RTyCon RTyVar r)
-> m r -> m (RTypeV 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 RTypeV Symbol RTyCon RTyVar r
t RTypeV Symbol RTyCon RTyVar r
t' r
r)
  = RTypeV Symbol RTyCon RTyVar r
-> RTypeV Symbol RTyCon RTyVar r
-> r
-> RTypeV Symbol RTyCon RTyVar r
forall v c tv r.
RTypeV v c tv r -> RTypeV v c tv r -> r -> RTypeV v c tv r
RAppTy (RTypeV Symbol RTyCon RTyVar r
 -> RTypeV Symbol RTyCon RTyVar r
 -> r
 -> RTypeV Symbol RTyCon RTyVar r)
-> m (RTypeV Symbol RTyCon RTyVar r)
-> m (RTypeV Symbol RTyCon RTyVar r
      -> r -> RTypeV Symbol RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool
-> RTypeV Symbol RTyCon RTyVar r
-> m (RTypeV Symbol RTyCon RTyVar r)
forall (m :: * -> *) a. Freshable m a => Bool -> a -> m a
refresh Bool
allowTC RTypeV Symbol RTyCon RTyVar r
t m (RTypeV Symbol RTyCon RTyVar r
   -> r -> RTypeV Symbol RTyCon RTyVar r)
-> m (RTypeV Symbol RTyCon RTyVar r)
-> m (r -> RTypeV 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
-> RTypeV Symbol RTyCon RTyVar r
-> m (RTypeV Symbol RTyCon RTyVar r)
forall (m :: * -> *) a. Freshable m a => Bool -> a -> m a
refresh Bool
allowTC RTypeV Symbol RTyCon RTyVar r
t' m (r -> RTypeV Symbol RTyCon RTyVar r)
-> m r -> m (RTypeV 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 RTypeV Symbol RTyCon RTyVar r
ty RTypeV 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, RTypeV Symbol RTyCon RTyVar r)]
e r
o Oblig
r RTypeV Symbol RTyCon RTyVar r
t)
  = [(Symbol, RTypeV Symbol RTyCon RTyVar r)]
-> r
-> Oblig
-> RTypeV Symbol RTyCon RTyVar r
-> RTypeV Symbol RTyCon RTyVar r
forall v c tv r.
[(Symbol, RTypeV v c tv r)]
-> r -> Oblig -> RTypeV v c tv r -> RTypeV v c tv r
RRTy [(Symbol, RTypeV Symbol RTyCon RTyVar r)]
e r
o Oblig
r (RTypeV Symbol RTyCon RTyVar r -> RTypeV Symbol RTyCon RTyVar r)
-> m (RTypeV Symbol RTyCon RTyVar r)
-> m (RTypeV Symbol RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool
-> RTypeV Symbol RTyCon RTyVar r
-> m (RTypeV Symbol RTyCon RTyVar r)
forall (m :: * -> *) r.
(Freshable m Integer, Freshable m r, Reftable r) =>
Bool -> RRType r -> m (RRType r)
refreshRefType Bool
allowTC RTypeV Symbol RTyCon RTyVar r
t

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

refreshRef :: (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. 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 -> 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 RTVUV Symbol RTyCon RTyVar
a SpecType
t RReft
r) =
  RTVUV Symbol RTyCon RTyVar -> SpecType -> RReft -> SpecType
forall v c tv r.
RTVUV v c tv -> RTypeV v c tv r -> r -> RTypeV v c tv r
RAllT RTVUV 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 PVUV Symbol RTyCon RTyVar
p SpecType
t) =
  PVUV Symbol RTyCon RTyVar -> SpecType -> SpecType
forall v c tv r. PVUV v c tv -> RTypeV v c tv r -> RTypeV v c tv r
RAllP PVUV 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 [RTPropV 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, 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 v c tv r. r -> RTypeV 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
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 v. v -> ExprV 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
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 v. v -> ExprV 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
forall a. Subable a => SubstV Symbol -> a -> a
F.subst [SubstV Symbol]
sus [RReft]
rs
       tr     <- refreshPs $ F.subst su tbd
       let t'  = RTypeRepV Symbol RTyCon RTyVar RReft -> SpecType
forall v c tv r. RTypeRepV v c tv r -> RTypeV v c tv r
fromRTypeRep (RTypeRepV Symbol RTyCon RTyVar RReft -> SpecType)
-> RTypeRepV Symbol RTyCon RTyVar RReft -> SpecType
forall a b. (a -> b) -> a -> b
$ RTypeRepV Symbol RTyCon RTyVar RReft
trep {ty_binds = xs', ty_args = ts', ty_res = tr, ty_refts = rs'}
       return (t', su)
    where
       trep :: RTypeRepV Symbol RTyCon RTyVar RReft
trep    = SpecType -> RTypeRepV Symbol RTyCon RTyVar RReft
forall v c tv r. RTypeV v c tv r -> RTypeRepV v c tv r
toRTypeRep SpecType
t
       xs :: [Symbol]
xs      = RTypeRepV Symbol RTyCon RTyVar RReft -> [Symbol]
forall v c tv r. RTypeRepV v c tv r -> [Symbol]
ty_binds RTypeRepV Symbol RTyCon RTyVar RReft
trep
       ts_u :: [SpecType]
ts_u    = RTypeRepV Symbol RTyCon RTyVar RReft -> [SpecType]
forall v c tv r. RTypeRepV v c tv r -> [RTypeV v c tv r]
ty_args  RTypeRepV Symbol RTyCon RTyVar RReft
trep
       tbd :: SpecType
tbd     = RTypeRepV Symbol RTyCon RTyVar RReft -> SpecType
forall v c tv r. RTypeRepV v c tv r -> RTypeV v c tv r
ty_res   RTypeRepV Symbol RTyCon RTyVar RReft
trep
       rs :: [RReft]
rs      = RTypeRepV Symbol RTyCon RTyVar RReft -> [RReft]
forall v c tv r. RTypeRepV v c tv r -> [r]
ty_refts RTypeRepV Symbol RTyCon RTyVar RReft
trep

refreshPs :: (FreshM m) => SpecType -> m SpecType
refreshPs :: forall (m :: * -> *). FreshM m => SpecType -> m SpecType
refreshPs = (RTPropV Symbol RTyCon RTyVar RReft
 -> m (RTPropV 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 RTPropV Symbol RTyCon RTyVar RReft
-> m (RTPropV Symbol 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
      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
F.mkSubst [(Symbol
y, Symbol -> Expr
forall v. v -> ExprV 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, 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, 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 :: (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) []