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

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

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

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


class (Applicative m, Monad m) => Freshable m a where
  fresh   :: m a
  true    :: Bool -> a -> m a
  true Bool
_  = forall (m :: * -> *) a. Monad m => a -> m a
return
  refresh :: Bool -> a -> m a
  refresh Bool
_ = 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" forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. Freshable m a => m a
fresh
    where
      kv :: Integer -> Expr
kv = (KVar -> Subst -> Expr
`F.PKVar` forall a. Monoid a => a
mempty) 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 = forall t. t -> [t]
single forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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                  = forall a. Maybe SrcSpan -> String -> a
panic forall a. Maybe a
Nothing String
"fresh Reft"
  true :: Bool -> Reft -> m Reft
true    Bool
_ (F.Reft (Symbol
v,Expr
_)) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ (Symbol, Expr) -> Reft
F.Reft (Symbol
v, forall a. Monoid a => a
mempty)
  refresh :: Bool -> Reft -> m Reft
refresh Bool
_ (F.Reft (Symbol
_,Expr
_)) = ((Symbol, Expr) -> Reft
F.Reft forall b c a. (b -> c) -> (a -> b) -> a -> c
.) forall b c a. (b -> c) -> (a -> b) -> a -> c
. (,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Symbol
freshVV forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *) a. Freshable m a => m a
fresh
    where
      freshVV :: m Symbol
freshVV            = Maybe Integer -> Symbol
F.vv forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. Freshable m a => m a
fresh

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

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

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

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

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

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

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

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

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

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

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

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

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

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


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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

refreshVV SpecType
t =
  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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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))
  = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp [(Symbol, b)]
ss (forall c tv r. r -> RType c tv r
RHole RReft
r)

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


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

refreshPs :: (FreshM m) => SpecType -> m SpecType
refreshPs :: forall (m :: * -> *). FreshM m => SpecType -> m SpecType
refreshPs = 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 forall (m :: * -> *) b.
Freshable m Integer =>
Ref b SpecType -> m (Ref b SpecType)
go
  where
    go :: Ref τ SpecType -> m (Ref τ SpecType)
go (RProp [(Symbol, τ)]
s SpecType
st) = do
      SpecType
t'    <- forall (m :: * -> *). FreshM m => SpecType -> m SpecType
refreshPs SpecType
st
      [Symbol]
xs    <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall a b. a -> b -> a
const 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, τ
_)) <- forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
xs [(Symbol, τ)]
s]
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp [(Symbol
x, τ
t) | (Symbol
x, (Symbol
_, τ
t)) <- forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
xs [(Symbol, τ)]
s] forall a b. (a -> b) -> a -> b
$ forall a. Subable a => Subst -> a -> a
F.subst Subst
su SpecType
t'

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

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

noHoles :: (F.Reftable r, TyConable c) => RType c tv r -> Bool
noHoles :: forall r c tv. (Reftable r, TyConable c) => RType c tv r -> Bool
noHoles = forall (t :: * -> *). Foldable t => t Bool -> Bool
and forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 (forall r. Reftable r => r -> Bool
hasHole r
r) forall a. a -> [a] -> [a]
: [Bool]
bs) []