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

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

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

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


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


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

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

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

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

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

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

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

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

trueRefType (RImpF Symbol
_ RRType r
t RRType r
t' r
_)
  = Symbol -> RRType r -> RRType r -> RRType r
forall r c tv.
Monoid r =>
Symbol -> RType c tv r -> RType c tv r -> RType c tv r
rImpF (Symbol -> RRType r -> RRType r -> RRType r)
-> m Symbol -> m (RRType r -> RRType r -> RRType 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 (RRType r -> RRType r -> RRType r)
-> m (RRType r) -> m (RRType r -> RRType r)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> RRType r -> m (RRType r)
forall (m :: * -> *) a. Freshable m a => a -> m a
true RRType r
t m (RRType r -> RRType r) -> m (RRType r) -> m (RRType r)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> RRType r -> m (RRType r)
forall (m :: * -> *) a. Freshable m a => a -> m a
true RRType r
t'

trueRefType (RFun Symbol
_ RRType r
t RRType r
t' r
_)
  = Symbol -> RRType r -> RRType r -> RRType r
forall r c tv.
Monoid r =>
Symbol -> RType c tv r -> RType c tv r -> RType c tv r
rFun (Symbol -> RRType r -> RRType r -> RRType r)
-> m Symbol -> m (RRType r -> RRType r -> RRType 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 (RRType r -> RRType r -> RRType r)
-> m (RRType r) -> m (RRType r -> RRType r)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> RRType r -> m (RRType r)
forall (m :: * -> *) a. Freshable m a => a -> m a
true RRType r
t m (RRType r -> RRType r) -> m (RRType r) -> m (RRType r)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> RRType r -> m (RRType r)
forall (m :: * -> *) a. Freshable m a => a -> m a
true RRType r
t'

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

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

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

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

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

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

trueRefType (REx Symbol
_ RRType r
t RRType r
t')
  = Symbol -> RRType r -> RRType r -> RRType r
forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> RType c tv r
REx (Symbol -> RRType r -> RRType r -> RRType r)
-> m Symbol -> m (RRType r -> RRType r -> RRType 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 (RRType r -> RRType r -> RRType r)
-> m (RRType r) -> m (RRType r -> RRType r)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> RRType r -> m (RRType r)
forall (m :: * -> *) a. Freshable m a => a -> m a
true RRType r
t m (RRType r -> RRType r) -> m (RRType r) -> m (RRType r)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> RRType r -> m (RRType r)
forall (m :: * -> *) a. Freshable m a => a -> m a
true RRType r
t'

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

trueRefType t :: RRType r
t@(RHole r
_)
  = RRType r -> m (RRType r)
forall (m :: * -> *) a. Monad m => a -> m a
return RRType r
t

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


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

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

refreshRefType (RImpF Symbol
b RRType r
t RRType r
t' r
_)
  | Symbol
b Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
F.dummySymbol = Symbol -> RRType r -> RRType r -> RRType r
forall r c tv.
Monoid r =>
Symbol -> RType c tv r -> RType c tv r -> RType c tv r
rImpF (Symbol -> RRType r -> RRType r -> RRType r)
-> m Symbol -> m (RRType r -> RRType r -> RRType 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 (RRType r -> RRType r -> RRType r)
-> m (RRType r) -> m (RRType r -> RRType r)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> RRType r -> m (RRType r)
forall (m :: * -> *) a. Freshable m a => a -> m a
refresh RRType r
t m (RRType r -> RRType r) -> m (RRType r) -> m (RRType r)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> RRType r -> m (RRType r)
forall (m :: * -> *) a. Freshable m a => a -> m a
refresh RRType r
t'
  | Bool
otherwise          = Symbol -> RRType r -> RRType r -> RRType r
forall r c tv.
Monoid r =>
Symbol -> RType c tv r -> RType c tv r -> RType c tv r
rImpF     Symbol
b     (RRType r -> RRType r -> RRType r)
-> m (RRType r) -> m (RRType r -> RRType r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RRType r -> m (RRType r)
forall (m :: * -> *) a. Freshable m a => a -> m a
refresh RRType r
t m (RRType r -> RRType r) -> m (RRType r) -> m (RRType r)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> RRType r -> m (RRType r)
forall (m :: * -> *) a. Freshable m a => a -> m a
refresh RRType r
t'

refreshRefType (RFun Symbol
b RRType r
t RRType r
t' r
_)
  | Symbol
b Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
F.dummySymbol = Symbol -> RRType r -> RRType r -> RRType r
forall r c tv.
Monoid r =>
Symbol -> RType c tv r -> RType c tv r -> RType c tv r
rFun (Symbol -> RRType r -> RRType r -> RRType r)
-> m Symbol -> m (RRType r -> RRType r -> RRType 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 (RRType r -> RRType r -> RRType r)
-> m (RRType r) -> m (RRType r -> RRType r)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> RRType r -> m (RRType r)
forall (m :: * -> *) a. Freshable m a => a -> m a
refresh RRType r
t m (RRType r -> RRType r) -> m (RRType r) -> m (RRType r)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> RRType r -> m (RRType r)
forall (m :: * -> *) a. Freshable m a => a -> m a
refresh RRType r
t'
  | Bool
otherwise          = Symbol -> RRType r -> RRType r -> RRType r
forall r c tv.
Monoid r =>
Symbol -> RType c tv r -> RType c tv r -> RType c tv r
rFun     Symbol
b     (RRType r -> RRType r -> RRType r)
-> m (RRType r) -> m (RRType r -> RRType r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RRType r -> m (RRType r)
forall (m :: * -> *) a. Freshable m a => a -> m a
refresh RRType r
t m (RRType r -> RRType r) -> m (RRType r) -> m (RRType r)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> RRType r -> m (RRType r)
forall (m :: * -> *) a. Freshable m a => a -> m a
refresh RRType r
t'

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

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

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

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

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

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

refreshRefType RRType r
t
  = RRType r -> m (RRType r)
forall (m :: * -> *) a. Monad m => a -> m a
return RRType r
t

refreshRef :: (F.Reftable r, Freshable f r, Freshable f Integer)
           => Ref τ (RType RTyCon RTyVar r) -> f (Ref τ (RRType r))
refreshRef :: Ref τ (RType RTyCon RTyVar r) -> f (Ref τ (RType RTyCon RTyVar r))
refreshRef (RProp [(Symbol, τ)]
_ (RHole r
_)) = Maybe SrcSpan -> String -> f (Ref τ (RType RTyCon RTyVar r))
forall a. Maybe SrcSpan -> String -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing String
"refreshRef: unexpected (RProp _ (RHole _))"
refreshRef (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)
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 (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> RType RTyCon RTyVar r -> f (RType RTyCon RTyVar r)
forall (m :: * -> *) r.
(Freshable m Integer, Freshable m r, Reftable r) =>
RRType r -> m (RRType r)
refreshRefType RType RTyCon RTyVar r
t

freshSym :: Freshable f a => (t, t1) -> f (a, t1)
freshSym :: (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 :: 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 (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 :: SpecType -> m SpecType
refreshVV (RAllT RTVU RTyCon RTyVar
a SpecType
t RReft
r) = 
  RTVU RTyCon RTyVar -> SpecType -> RReft -> SpecType
forall c tv r. RTVU c tv -> RType c tv r -> r -> RType c tv r
RAllT RTVU RTyCon RTyVar
a (SpecType -> RReft -> SpecType)
-> m SpecType -> m (RReft -> SpecType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SpecType -> m SpecType
forall (m :: * -> *). FreshM m => SpecType -> m SpecType
refreshVV SpecType
t m (RReft -> SpecType) -> m RReft -> m SpecType
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> RReft -> m RReft
forall (m :: * -> *) a. Monad m => a -> m a
return RReft
r 

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

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

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

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

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

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

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

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

refreshVVRef (RProp [(Symbol, b)]
ss SpecType
t)
  = do [Symbol]
xs    <- (Symbol -> m Symbol) -> [Symbol] -> m [Symbol]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
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, b) -> Symbol
forall a b. (a, b) -> a
fst ((Symbol, b) -> Symbol) -> [(Symbol, b)] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, b)]
ss)
       let su :: Subst
su = [(Symbol, Expr)] -> Subst
F.mkSubst ([(Symbol, Expr)] -> Subst) -> [(Symbol, Expr)] -> Subst
forall a b. (a -> b) -> a -> b
$ [Symbol] -> [Expr] -> [(Symbol, Expr)]
forall a b. [a] -> [b] -> [(a, b)]
zip ((Symbol, b) -> Symbol
forall a b. (a, b) -> a
fst ((Symbol, b) -> Symbol) -> [(Symbol, b)] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, b)]
ss) (Symbol -> Expr
F.EVar (Symbol -> Expr) -> [Symbol] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
xs)
       ([(Symbol, b)] -> SpecType -> Ref b SpecType
forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp ([Symbol] -> [b] -> [(Symbol, b)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
xs ((Symbol, b) -> b
forall a b. (a, b) -> b
snd ((Symbol, b) -> b) -> [(Symbol, b)] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, b)]
ss)) (SpecType -> Ref b SpecType)
-> (SpecType -> SpecType) -> SpecType -> Ref b SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Subst -> SpecType -> SpecType
forall a. Subable a => Subst -> a -> a
F.subst Subst
su) (SpecType -> Ref b SpecType) -> m SpecType -> m (Ref b 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

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


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

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

--------------------------------------------------------------------------------
refreshHoles :: (F.Symbolic t, F.Reftable r, TyConable c, Freshable f r)
             => [(t, RType c tv r)] -> f ([F.Symbol], [(t, RType c tv r)])
refreshHoles :: [(t, RType c tv r)] -> f ([Symbol], [(t, RType c tv r)])
refreshHoles [(t, RType c tv r)]
vts = ([Maybe Symbol] -> [Symbol])
-> ([Maybe Symbol], [(t, RType c tv r)])
-> ([Symbol], [(t, RType c tv r)])
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)
mapM (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) =>
(a, RType c tv r) -> m (Maybe Symbol, a, RType c tv r)
refreshHoles' [(t, RType c tv r)]
vts
  where
  --   extract :: (t, t1, t2) -> (t, (t1, t2))
    extract :: (a, a, b) -> (a, (a, b))
extract (a
a,a
b,b
c) = (a
a,(a
b,b
c))

refreshHoles' :: (F.Symbolic a, F.Reftable r, TyConable c, Freshable m r)
              => (a, RType c tv r) -> m (Maybe F.Symbol, a, RType c tv r)
refreshHoles' :: (a, RType c tv r) -> m (Maybe Symbol, a, RType c tv r)
refreshHoles' (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 (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 = a -> m a
forall (m :: * -> *) a. Freshable m a => a -> m a
refresh a
r
         | Bool
otherwise = a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
r

noHoles :: (F.Reftable r, TyConable c) => RType c tv r -> Bool
noHoles :: 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) []