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

{-# OPTIONS_GHC -Wno-orphans #-}

module Language.Haskell.Liquid.Constraint.Fresh
  ( -- module Language.Haskell.Liquid.Types.Fresh
    -- ,
    refreshArgsTop
  , freshTyType
  , freshTyExpr
  , trueTy
  , addKuts
  )
  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           Prelude                        hiding (error)

import qualified Language.Fixpoint.Types as F
import           Language.Fixpoint.Types.Visitor (kvarsExpr)
import           Language.Haskell.Liquid.Types.Fresh
import           Language.Haskell.Liquid.Types.RefType
import           Language.Haskell.Liquid.Types.RType
import           Language.Haskell.Liquid.Types.RTypeOp
import           Language.Haskell.Liquid.Types.Types
import           Language.Haskell.Liquid.Constraint.Types
import qualified Language.Haskell.Liquid.GHC.Misc as GM
import           Language.Haskell.Liquid.UX.Config
import           Liquid.GHC.API as Ghc hiding (get)

--------------------------------------------------------------------------------
-- | This is all hardwiring stuff to CG ----------------------------------------
--------------------------------------------------------------------------------
instance Freshable CG Integer where
  fresh :: CG Integer
fresh = do s <- StateT CGInfo Identity CGInfo
forall s (m :: * -> *). MonadState s m => m s
get
             let n = CGInfo -> Integer
freshIndex CGInfo
s
             put $ s { freshIndex = n + 1 }
             return n

--------------------------------------------------------------------------------
refreshArgsTop :: (Var, SpecType) -> CG SpecType
--------------------------------------------------------------------------------
refreshArgsTop :: (Var,
 RTypeBV
   Symbol
   Symbol
   RTyCon
   RTyVar
   (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
-> CG
     (RTypeBV
        Symbol
        Symbol
        RTyCon
        RTyVar
        (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
refreshArgsTop (Var
x, RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
t)
  = do (t', su) <- RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> StateT
     CGInfo
     Identity
     (RTypeBV
        Symbol
        Symbol
        RTyCon
        RTyVar
        (UReftBV Symbol Symbol (ReftBV Symbol Symbol)),
      Subst)
forall (m :: * -> *).
FreshM m =>
RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> m (RTypeBV
        Symbol
        Symbol
        RTyCon
        RTyVar
        (UReftBV Symbol Symbol (ReftBV Symbol Symbol)),
      Subst)
refreshArgsSub RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
t
       modify $ \CGInfo
s -> CGInfo
s {termExprs = M.adjust (F.subst su <$>) x $ termExprs s}
       return t'

--------------------------------------------------------------------------------
-- | Generation: Freshness -----------------------------------------------------
--------------------------------------------------------------------------------

-- | Right now, we generate NO new pvars. Rather than clutter code
--   with `uRType` calls, put it in one place where the above
--   invariant is /obviously/ enforced.
--   Constraint generation should ONLY use @freshTyType@ and @freshTyExpr@

freshTyType        :: Bool -> KVKind -> CoreExpr -> Type -> CG SpecType
freshTyType :: Bool
-> KVKind
-> Expr Var
-> Type
-> CG
     (RTypeBV
        Symbol
        Symbol
        RTyCon
        RTyVar
        (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
freshTyType Bool
allowTC KVKind
k Expr Var
e Type
τ  =  [Char]
-> RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
forall a. PPrint a => [Char] -> a -> a
F.notracepp ([Char]
"freshTyType: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ KVKind -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp KVKind
k [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Expr Var -> [Char]
forall a. Outputable a => a -> [Char]
GM.showPpr Expr Var
e)
                   (RTypeBV
   Symbol
   Symbol
   RTyCon
   RTyVar
   (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
 -> RTypeBV
      Symbol
      Symbol
      RTyCon
      RTyVar
      (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
-> CG
     (RTypeBV
        Symbol
        Symbol
        RTyCon
        RTyVar
        (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
-> CG
     (RTypeBV
        Symbol
        Symbol
        RTyCon
        RTyVar
        (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool
-> KVKind
-> RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> CG
     (RTypeBV
        Symbol
        Symbol
        RTyCon
        RTyVar
        (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
freshTyReftype Bool
allowTC KVKind
k (Type
-> RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
forall r. IsReft r => Type -> RRType r
ofType Type
τ)

freshTyExpr        :: Bool -> KVKind -> CoreExpr -> Type -> CG SpecType
freshTyExpr :: Bool
-> KVKind
-> Expr Var
-> Type
-> CG
     (RTypeBV
        Symbol
        Symbol
        RTyCon
        RTyVar
        (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
freshTyExpr Bool
allowTC KVKind
k Expr Var
e Type
_  = Bool
-> KVKind
-> RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> CG
     (RTypeBV
        Symbol
        Symbol
        RTyCon
        RTyVar
        (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
freshTyReftype Bool
allowTC KVKind
k (RTypeBV
   Symbol
   Symbol
   RTyCon
   RTyVar
   (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
 -> CG
      (RTypeBV
         Symbol
         Symbol
         RTyCon
         RTyVar
         (UReftBV Symbol Symbol (ReftBV Symbol Symbol))))
-> RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> CG
     (RTypeBV
        Symbol
        Symbol
        RTyCon
        RTyVar
        (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
forall a b. (a -> b) -> a -> b
$ Expr Var
-> RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
exprRefType Expr Var
e

freshTyReftype     :: Bool -> KVKind -> SpecType -> CG SpecType
freshTyReftype :: Bool
-> KVKind
-> RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> CG
     (RTypeBV
        Symbol
        Symbol
        RTyCon
        RTyVar
        (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
freshTyReftype Bool
allowTC KVKind
k RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
t = do
    st <- RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> CG
     (RTypeBV
        Symbol
        Symbol
        RTyCon
        RTyVar
        (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
fixTy RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
t CG
  (RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
-> (RTypeBV
      Symbol
      Symbol
      RTyCon
      RTyVar
      (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
    -> CG
         (RTypeBV
            Symbol
            Symbol
            RTyCon
            RTyVar
            (UReftBV Symbol Symbol (ReftBV Symbol Symbol))))
-> CG
     (RTypeBV
        Symbol
        Symbol
        RTyCon
        RTyVar
        (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
forall a b.
StateT CGInfo Identity a
-> (a -> StateT CGInfo Identity b) -> StateT CGInfo Identity b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Bool
-> RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> CG
     (RTypeBV
        Symbol
        Symbol
        RTyCon
        RTyVar
        (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
forall (m :: * -> *) a. Freshable m a => Bool -> a -> m a
refresh Bool
allowTC
    addKVars k st
    return st

-- | Used to generate "cut" kvars for fixpoint. Typically, KVars for recursive
--   definitions, and also to update the KVar profile.
addKVars        :: KVKind -> SpecType -> CG ()
addKVars :: KVKind
-> RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> StateT CGInfo Identity ()
addKVars !KVKind
k !RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
t  = do
    cfg <- (CGInfo -> Config) -> StateT CGInfo Identity Config
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (TargetInfo -> Config
forall t. HasConfig t => t -> Config
getConfig (TargetInfo -> Config)
-> (CGInfo -> TargetInfo) -> CGInfo -> Config
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CGInfo -> TargetInfo
ghcI)
    when True          $ modify $ \CGInfo
s -> CGInfo
s { kvProf = updKVProf k ks (kvProf s) }
    when (isKut cfg k) $ addKuts k t
  where
    ks :: Kuts
ks         = HashSet KVar -> Kuts
F.KS (HashSet KVar -> Kuts) -> HashSet KVar -> Kuts
forall a b. (a -> b) -> a -> b
$ [KVar] -> HashSet KVar
forall a. Hashable a => [a] -> HashSet a
S.fromList ([KVar] -> HashSet KVar) -> [KVar] -> HashSet KVar
forall a b. (a -> b) -> a -> b
$ RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> [KVar]
specTypeKVars RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
t

isKut :: Config -> KVKind -> Bool
isKut :: Config -> KVKind -> Bool
isKut Config
_  (RecBindE Var
_) = Bool
True
isKut Config
cfg KVKind
ProjectE    = Bool -> Bool
not (Config -> Bool
forall t. HasConfig t => t -> Bool
higherOrderFlag Config
cfg) -- see ISSUE 1034, tests/pos/T1034.hs
isKut Config
_    KVKind
_          = Bool
False

addKuts :: (PPrint a) => a -> SpecType -> CG ()
addKuts :: forall a.
PPrint a =>
a
-> RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> StateT CGInfo Identity ()
addKuts a
_x RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
t = (CGInfo -> CGInfo) -> StateT CGInfo Identity ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((CGInfo -> CGInfo) -> StateT CGInfo Identity ())
-> (CGInfo -> CGInfo) -> StateT CGInfo Identity ()
forall a b. (a -> b) -> a -> b
$ \CGInfo
s -> CGInfo
s { kuts = mappend (F.KS ks) (kuts s)   }
  where
     ks' :: HashSet KVar
ks'     = [KVar] -> HashSet KVar
forall a. Hashable a => [a] -> HashSet a
S.fromList ([KVar] -> HashSet KVar) -> [KVar] -> HashSet KVar
forall a b. (a -> b) -> a -> b
$ RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> [KVar]
specTypeKVars RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
t
     ks :: HashSet KVar
ks
       | HashSet KVar -> Bool
forall a. HashSet a -> Bool
S.null HashSet KVar
ks' = HashSet KVar
ks'
       | Bool
otherwise  = {- F.tracepp ("addKuts: " ++ showpp _x) -} HashSet KVar
ks'

specTypeKVars :: SpecType -> [F.KVar]
specTypeKVars :: RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> [KVar]
specTypeKVars = Bool
-> (SEnvB
      Symbol
      (RTypeBV
         Symbol
         Symbol
         RTyCon
         RTyVar
         (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
    -> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
    -> [KVar]
    -> [KVar])
-> [KVar]
-> RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> [KVar]
forall r c b v tv z.
(IsReft r, TyConable c, Binder b, ReftBind r ~ b) =>
Bool
-> (SEnvB b (RTypeBV b v c tv r) -> r -> z -> z)
-> z
-> RTypeBV b v c tv r
-> z
foldReft Bool
False (\ SEnvB
  Symbol
  (RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
_ UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r [KVar]
ks -> Expr -> [KVar]
forall v. ExprV v -> [KVar]
kvarsExpr (ReftBV Symbol Symbol -> Expr
forall b v. ReftBV b v -> ExprBV b v
F.reftPred (ReftBV Symbol Symbol -> Expr) -> ReftBV Symbol Symbol -> Expr
forall a b. (a -> b) -> a -> b
$ UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> ReftBV Symbol Symbol
forall b v r. UReftBV b v r -> r
ur_reft UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r) [KVar] -> [KVar] -> [KVar]
forall a. [a] -> [a] -> [a]
++ [KVar]
ks) []

--------------------------------------------------------------------------------
trueTy  :: Bool -> Type -> CG SpecType
--------------------------------------------------------------------------------
trueTy :: Bool
-> Type
-> CG
     (RTypeBV
        Symbol
        Symbol
        RTyCon
        RTyVar
        (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
trueTy Bool
allowTC = Type
-> CG
     (RTypeBV
        Symbol
        Symbol
        RTyCon
        RTyVar
        (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
ofType' (Type
 -> CG
      (RTypeBV
         Symbol
         Symbol
         RTyCon
         RTyVar
         (UReftBV Symbol Symbol (ReftBV Symbol Symbol))))
-> (RTypeBV
      Symbol
      Symbol
      RTyCon
      RTyVar
      (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
    -> CG
         (RTypeBV
            Symbol
            Symbol
            RTyCon
            RTyVar
            (UReftBV Symbol Symbol (ReftBV Symbol Symbol))))
-> Type
-> CG
     (RTypeBV
        Symbol
        Symbol
        RTyCon
        RTyVar
        (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Bool
-> RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> CG
     (RTypeBV
        Symbol
        Symbol
        RTyCon
        RTyVar
        (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
forall (m :: * -> *) a. Freshable m a => Bool -> a -> m a
true Bool
allowTC

ofType' :: Type -> CG SpecType
ofType' :: Type
-> CG
     (RTypeBV
        Symbol
        Symbol
        RTyCon
        RTyVar
        (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
ofType' = RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> CG
     (RTypeBV
        Symbol
        Symbol
        RTyCon
        RTyVar
        (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
fixTy (RTypeBV
   Symbol
   Symbol
   RTyCon
   RTyVar
   (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
 -> CG
      (RTypeBV
         Symbol
         Symbol
         RTyCon
         RTyVar
         (UReftBV Symbol Symbol (ReftBV Symbol Symbol))))
-> (Type
    -> RTypeBV
         Symbol
         Symbol
         RTyCon
         RTyVar
         (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
-> Type
-> CG
     (RTypeBV
        Symbol
        Symbol
        RTyCon
        RTyVar
        (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type
-> RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
forall r. IsReft r => Type -> RRType r
ofType

fixTy :: SpecType -> CG SpecType
fixTy :: RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> CG
     (RTypeBV
        Symbol
        Symbol
        RTyCon
        RTyVar
        (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
fixTy RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
t = do tyi   <- (CGInfo -> TyConMap) -> StateT CGInfo Identity TyConMap
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CGInfo -> TyConMap
tyConInfo
             tce   <- gets tyConEmbed
             return $ addTyConInfo tce tyi t

exprRefType :: CoreExpr -> SpecType
exprRefType :: Expr Var
-> RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
exprRefType = HashMap
  Var
  (RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
-> Expr Var
-> RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
exprRefType_ HashMap
  Var
  (RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
forall k v. HashMap k v
M.empty

exprRefType_ :: M.HashMap Var SpecType -> CoreExpr -> SpecType
exprRefType_ :: HashMap
  Var
  (RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
-> Expr Var
-> RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
exprRefType_ HashMap
  Var
  (RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
γ (Let Bind Var
b Expr Var
e)
  = HashMap
  Var
  (RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
-> Expr Var
-> RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
exprRefType_ (HashMap
  Var
  (RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
-> Bind Var
-> HashMap
     Var
     (RTypeBV
        Symbol
        Symbol
        RTyCon
        RTyVar
        (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
bindRefType_ HashMap
  Var
  (RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
γ Bind Var
b) Expr Var
e

exprRefType_ HashMap
  Var
  (RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
γ (Lam Var
α Expr Var
e) | Var -> Bool
isTyVar Var
α
  = RTVUBV Symbol Symbol RTyCon RTyVar
-> RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
forall b v c tv r.
RTVUBV b v c tv -> RTypeBV b v c tv r -> r -> RTypeBV b v c tv r
RAllT (RTyVar -> RTVUBV Symbol Symbol RTyCon RTyVar
forall tv s. tv -> RTVar tv s
makeRTVar (RTyVar -> RTVUBV Symbol Symbol RTyCon RTyVar)
-> RTyVar -> RTVUBV Symbol Symbol RTyCon RTyVar
forall a b. (a -> b) -> a -> b
$ Var -> RTyVar
rTyVar Var
α) (HashMap
  Var
  (RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
-> Expr Var
-> RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
exprRefType_ HashMap
  Var
  (RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
γ Expr Var
e) UReftBV Symbol Symbol (ReftBV Symbol Symbol)
forall a. Monoid a => a
mempty

exprRefType_ HashMap
  Var
  (RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
γ (Lam Var
x Expr Var
e)
  = Symbol
-> RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
forall r b v c tv.
IsReft r =>
b -> RTypeBV b v c tv r -> RTypeBV b v c tv r -> RTypeBV b v c tv r
rFun (Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
x) (Type
-> RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
forall r. IsReft r => Type -> RRType r
ofType (Type
 -> RTypeBV
      Symbol
      Symbol
      RTyCon
      RTyVar
      (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
-> Type
-> RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
forall a b. (a -> b) -> a -> b
$ Var -> Type
varType Var
x) (HashMap
  Var
  (RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
-> Expr Var
-> RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
exprRefType_ HashMap
  Var
  (RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
γ Expr Var
e)

exprRefType_ HashMap
  Var
  (RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
γ (Tick CoreTickish
_ Expr Var
e)
  = HashMap
  Var
  (RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
-> Expr Var
-> RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
exprRefType_ HashMap
  Var
  (RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
γ Expr Var
e

exprRefType_ HashMap
  Var
  (RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
γ (Var Var
x)
  = RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> Var
-> HashMap
     Var
     (RTypeBV
        Symbol
        Symbol
        RTyCon
        RTyVar
        (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
-> RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
forall k v. Hashable k => v -> k -> HashMap k v -> v
M.lookupDefault (Type
-> RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
forall r. IsReft r => Type -> RRType r
ofType (Type
 -> RTypeBV
      Symbol
      Symbol
      RTyCon
      RTyVar
      (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
-> Type
-> RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
forall a b. (a -> b) -> a -> b
$ Var -> Type
varType Var
x) Var
x HashMap
  Var
  (RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
γ

exprRefType_ HashMap
  Var
  (RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
_ Expr Var
e
  = Type
-> RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
forall r. IsReft r => Type -> RRType r
ofType (Type
 -> RTypeBV
      Symbol
      Symbol
      RTyCon
      RTyVar
      (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
-> Type
-> RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
forall a b. (a -> b) -> a -> b
$ HasDebugCallStack => Expr Var -> Type
Expr Var -> Type
exprType Expr Var
e

bindRefType_ :: M.HashMap Var SpecType -> Bind Var -> M.HashMap Var SpecType
bindRefType_ :: HashMap
  Var
  (RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
-> Bind Var
-> HashMap
     Var
     (RTypeBV
        Symbol
        Symbol
        RTyCon
        RTyVar
        (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
bindRefType_ HashMap
  Var
  (RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
γ (Rec [(Var, Expr Var)]
xes)
  = HashMap
  Var
  (RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
-> [(Var,
     RTypeBV
       Symbol
       Symbol
       RTyCon
       RTyVar
       (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))]
-> HashMap
     Var
     (RTypeBV
        Symbol
        Symbol
        RTyCon
        RTyVar
        (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
forall k (t :: * -> *) v.
(Eq k, Foldable t, Hashable k) =>
HashMap k v -> t (k, v) -> HashMap k v
extendγ HashMap
  Var
  (RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
γ [(Var
x, HashMap
  Var
  (RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
-> Expr Var
-> RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
exprRefType_ HashMap
  Var
  (RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
γ Expr Var
e) | (Var
x,Expr Var
e) <- [(Var, Expr Var)]
xes]

bindRefType_ HashMap
  Var
  (RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
γ (NonRec Var
x Expr Var
e)
  = HashMap
  Var
  (RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
-> [(Var,
     RTypeBV
       Symbol
       Symbol
       RTyCon
       RTyVar
       (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))]
-> HashMap
     Var
     (RTypeBV
        Symbol
        Symbol
        RTyCon
        RTyVar
        (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
forall k (t :: * -> *) v.
(Eq k, Foldable t, Hashable k) =>
HashMap k v -> t (k, v) -> HashMap k v
extendγ HashMap
  Var
  (RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
γ [(Var
x, HashMap
  Var
  (RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
-> Expr Var
-> RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
exprRefType_ HashMap
  Var
  (RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
γ Expr Var
e)]

extendγ :: (Eq k, Foldable t, Hashable k)
        => M.HashMap k v
        -> t (k, v)
        -> M.HashMap k v
extendγ :: forall k (t :: * -> *) v.
(Eq k, Foldable t, Hashable k) =>
HashMap k v -> t (k, v) -> HashMap k v
extendγ HashMap k v
γ t (k, v)
xts
  = ((k, v) -> HashMap k v -> HashMap k v)
-> HashMap k v -> t (k, v) -> HashMap k v
forall a b. (a -> b -> b) -> b -> t a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\(k
x,v
t) HashMap k v
m -> k -> v -> HashMap k v -> HashMap k v
forall k v. Hashable k => k -> v -> HashMap k v -> HashMap k v
M.insert k
x v
t HashMap k v
m) HashMap k v
γ t (k, v)
xts