{-# LANGUAGE OverloadedStrings     #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE TypeOperators         #-}

{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}

--------------------------------------------------------------------------------
-- | Constraint Splitting ------------------------------------------------------
--------------------------------------------------------------------------------

module Language.Haskell.Liquid.Constraint.Split (

  -- * Split Subtyping Constraints
    splitC

  -- * Split Well-formedness Constraints
  , splitW

  -- * ???
  , envToSub

  -- * Panic
  , panicUnbound
  ) where

import           Prelude hiding (error)



import           Text.PrettyPrint.HughesPJ hiding (first, parens)

import           Data.Maybe          (fromMaybe)
import           Control.Monad
import           Control.Monad.State (gets)
import qualified Control.Exception as Ex

import qualified Language.Fixpoint.Types            as F
import           Language.Fixpoint.Misc hiding (errorstar)
import           Language.Fixpoint.SortCheck (pruneUnsortedReft)

import           Language.Haskell.Liquid.Misc -- (concatMapM)
import qualified Language.Haskell.Liquid.UX.CTags       as Tg
import           Language.Haskell.Liquid.Types.Errors
import           Language.Haskell.Liquid.Types.Fresh
import           Language.Haskell.Liquid.Types.PredType
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.Types.Variance
import           Language.Haskell.Liquid.UX.Config
import           Language.Haskell.Liquid.UX.Tidy ()


import           Language.Haskell.Liquid.Constraint.Types
import           Language.Haskell.Liquid.Constraint.Env
import           Language.Haskell.Liquid.Constraint.Constraint
import           Language.Haskell.Liquid.Constraint.Monad (envToSub)

--------------------------------------------------------------------------------
splitW ::  WfC -> CG [FixWfC]
--------------------------------------------------------------------------------
splitW :: WfC -> CG [FixWfC]
splitW (WfC CGEnv
γ t :: RTypeBV Symbol Symbol RTyCon RTyVar RReft
t@(RFun Symbol
x RFInfo
_ RTypeBV Symbol Symbol RTyCon RTyVar RReft
t1 RTypeBV Symbol Symbol RTyCon RTyVar RReft
t2 RReft
_))
  =  do ws'  <- WfC -> CG [FixWfC]
splitW (CGEnv -> RTypeBV Symbol Symbol RTyCon RTyVar RReft -> WfC
WfC CGEnv
γ RTypeBV Symbol Symbol RTyCon RTyVar RReft
t1)
        γ'   <- γ += ("splitW", x, t1)
        ws   <- bsplitW γ t
        ws'' <- splitW (WfC γ' t2)
        return $ ws ++ ws' ++ ws''

splitW (WfC CGEnv
γ t :: RTypeBV Symbol Symbol RTyCon RTyVar RReft
t@(RAppTy RTypeBV Symbol Symbol RTyCon RTyVar RReft
t1 RTypeBV Symbol Symbol RTyCon RTyVar RReft
t2 RReft
_))
  =  do ws   <- CGEnv -> RTypeBV Symbol Symbol RTyCon RTyVar RReft -> CG [FixWfC]
bsplitW CGEnv
γ RTypeBV Symbol Symbol RTyCon RTyVar RReft
t
        ws'  <- splitW (WfC γ t1)
        ws'' <- splitW (WfC γ t2)
        return $ ws ++ ws' ++ ws''

splitW (WfC CGEnv
γ t' :: RTypeBV Symbol Symbol RTyCon RTyVar RReft
t'@(RAllT RTVar RTyVar (RType RTyCon RTyVar NoReft)
a RTypeBV Symbol Symbol RTyCon RTyVar RReft
t RReft
_))
  = do γ'  <- CGEnv -> RTVar RTyVar (RType RTyCon RTyVar NoReft) -> CG CGEnv
forall b0.
CGEnv -> RTVar RTyVar (RType RTyCon RTyVar b0) -> CG CGEnv
updateEnv CGEnv
γ RTVar RTyVar (RType RTyCon RTyVar NoReft)
a
       ws  <- bsplitW γ t'
       ws' <- splitW (WfC γ' t)
       return $ ws ++ ws'

splitW (WfC CGEnv
γ (RAllP PVUBV Symbol Symbol RTyCon RTyVar
_ RTypeBV Symbol Symbol RTyCon RTyVar RReft
r))
  = WfC -> CG [FixWfC]
splitW (CGEnv -> RTypeBV Symbol Symbol RTyCon RTyVar RReft -> WfC
WfC CGEnv
γ RTypeBV Symbol Symbol RTyCon RTyVar RReft
r)

splitW (WfC CGEnv
γ t :: RTypeBV Symbol Symbol RTyCon RTyVar RReft
t@(RVar RTyVar
_ RReft
_))
  = CGEnv -> RTypeBV Symbol Symbol RTyCon RTyVar RReft -> CG [FixWfC]
bsplitW CGEnv
γ RTypeBV Symbol Symbol RTyCon RTyVar RReft
t

splitW (WfC CGEnv
γ t :: RTypeBV Symbol Symbol RTyCon RTyVar RReft
t@(RApp RTyCon
_ [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
ts [RTPropBV Symbol Symbol RTyCon RTyVar RReft]
rs RReft
_))
  =  do ws    <- CGEnv -> RTypeBV Symbol Symbol RTyCon RTyVar RReft -> CG [FixWfC]
bsplitW CGEnv
γ RTypeBV Symbol Symbol RTyCon RTyVar RReft
t
        γ'    <- if bscope (getConfig γ) then γ `extendEnvWithVV` t else return γ
        ws'   <- concat <$> mapM (splitW . WfC γ') ts
        ws''  <- concat <$> mapM (rsplitW γ)       rs
        return $ ws ++ ws' ++ ws''

splitW (WfC CGEnv
γ (RAllE Symbol
x RTypeBV Symbol Symbol RTyCon RTyVar RReft
tx RTypeBV Symbol Symbol RTyCon RTyVar RReft
t))
  = do  ws  <- WfC -> CG [FixWfC]
splitW (CGEnv -> RTypeBV Symbol Symbol RTyCon RTyVar RReft -> WfC
WfC CGEnv
γ RTypeBV Symbol Symbol RTyCon RTyVar RReft
tx)
        γ'  <- γ += ("splitW1", x, tx)
        ws' <- splitW (WfC γ' t)
        return $ ws ++ ws'

splitW (WfC CGEnv
γ (REx Symbol
x RTypeBV Symbol Symbol RTyCon RTyVar RReft
tx RTypeBV Symbol Symbol RTyCon RTyVar RReft
t))
  = do  ws  <- WfC -> CG [FixWfC]
splitW (CGEnv -> RTypeBV Symbol Symbol RTyCon RTyVar RReft -> WfC
WfC CGEnv
γ RTypeBV Symbol Symbol RTyCon RTyVar RReft
tx)
        γ'  <- γ += ("splitW2", x, tx)
        ws' <- splitW (WfC γ' t)
        return $ ws ++ ws'

splitW (WfC CGEnv
γ (RRTy [(Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
_ RReft
_ Oblig
_ RTypeBV Symbol Symbol RTyCon RTyVar RReft
t))
  = WfC -> CG [FixWfC]
splitW (CGEnv -> RTypeBV Symbol Symbol RTyCon RTyVar RReft -> WfC
WfC CGEnv
γ RTypeBV Symbol Symbol RTyCon RTyVar RReft
t)

splitW (WfC CGEnv
_ RTypeBV Symbol Symbol RTyCon RTyVar RReft
t)
  = Maybe SrcSpan -> [Char] -> CG [FixWfC]
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing ([Char] -> CG [FixWfC]) -> [Char] -> CG [FixWfC]
forall a b. (a -> b) -> a -> b
$ [Char]
"splitW cannot handle: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ RTypeBV Symbol Symbol RTyCon RTyVar RReft -> [Char]
forall a. PPrint a => a -> [Char]
showpp RTypeBV Symbol Symbol RTyCon RTyVar RReft
t

rsplitW :: CGEnv
        -> Ref RSort SpecType
        -> CG [FixWfC]
rsplitW :: CGEnv -> RTPropBV Symbol Symbol RTyCon RTyVar RReft -> CG [FixWfC]
rsplitW CGEnv
_ (RProp [(Symbol, RType RTyCon RTyVar NoReft)]
_ (RHole RReft
_)) =
  Maybe SrcSpan -> [Char] -> CG [FixWfC]
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing [Char]
"Constrains: rsplitW for RProp _ (RHole _)"

rsplitW CGEnv
γ (RProp [(Symbol, RType RTyCon RTyVar NoReft)]
ss RTypeBV Symbol Symbol RTyCon RTyVar RReft
t0) = do
  γ' <- (CGEnv
 -> ([Char], Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)
 -> CG CGEnv)
-> CGEnv
-> [([Char], Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
-> CG CGEnv
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM CGEnv
-> ([Char], Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> CG CGEnv
(+=) CGEnv
γ [([Char]
"rsplitW", Symbol
x, RType RTyCon RTyVar NoReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall r b v c tv.
IsReft r =>
RTypeBV b v c tv (NoReftB b) -> RTypeBV b v c tv r
ofRSort RType RTyCon RTyVar NoReft
s) | (Symbol
x, RType RTyCon RTyVar NoReft
s) <- [(Symbol, RType RTyCon RTyVar NoReft)]
ss]
  splitW $ WfC γ' t0


bsplitW :: CGEnv -> SpecType -> CG [FixWfC]
bsplitW :: CGEnv -> RTypeBV Symbol Symbol RTyCon RTyVar RReft -> CG [FixWfC]
bsplitW CGEnv
γ RTypeBV Symbol Symbol RTyCon RTyVar RReft
t =
  do temp  <- CG Templates
getTemplates
     isHO  <- gets allowHO
     return $ bsplitW' γ t temp isHO

bsplitW' :: (PPrint r, IsReft r, ReftBind r ~ F.Symbol, ReftVar r ~ F.Symbol, SubsTy RTyVar RSort r)
         => CGEnv -> RRType r -> F.Templates -> Bool -> [F.WfC Cinfo]
bsplitW' :: forall r.
(PPrint r, IsReft r, ReftBind r ~ Symbol, ReftVar r ~ Symbol,
 SubsTy RTyVar (RType RTyCon RTyVar NoReft) r) =>
CGEnv -> RRType r -> Templates -> Bool -> [FixWfC]
bsplitW' CGEnv
γ RRType r
t Templates
temp Bool
isHO
  | Bool
isHO Bool -> Bool -> Bool
|| SortedReft -> Bool
F.isNonTrivial SortedReft
r'
  = IBindEnv -> SortedReft -> Cinfo -> [FixWfC]
forall a. Fixpoint a => IBindEnv -> SortedReft -> a -> [WfC a]
F.wfC (FEnv -> IBindEnv
feBinds (FEnv -> IBindEnv) -> FEnv -> IBindEnv
forall a b. (a -> b) -> a -> b
$ CGEnv -> FEnv
fenv CGEnv
γ) SortedReft
r' Cinfo
ci
  | Bool
otherwise
  = []
  where
    r' :: SortedReft
r'                = CGEnv -> Templates -> RRType r -> SortedReft
forall r.
(PPrint r, IsReft r, ReftBind r ~ Symbol, ReftVar r ~ Symbol,
 SubsTy RTyVar (RType RTyCon RTyVar NoReft) r) =>
CGEnv -> Templates -> RRType r -> SortedReft
rTypeSortedReft' CGEnv
γ Templates
temp RRType r
t
    ci :: Cinfo
ci                = SrcSpan -> Maybe Error -> Maybe Var -> Cinfo
Ci (CGEnv -> SrcSpan
getLocation CGEnv
γ) Maybe Error
forall a. Maybe a
Nothing (CGEnv -> Maybe Var
cgVar CGEnv
γ)

splitfWithVariance :: Applicative f
                   => (t -> t -> f [a]) -> t -> t -> Variance -> f [a]
splitfWithVariance :: forall (f :: * -> *) t a.
Applicative f =>
(t -> t -> f [a]) -> t -> t -> Variance -> f [a]
splitfWithVariance t -> t -> f [a]
f t
t1 t
t2 Variance
Invariant     = [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
(++) ([a] -> [a] -> [a]) -> f [a] -> f ([a] -> [a])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> t -> t -> f [a]
f t
t1 t
t2 f ([a] -> [a]) -> f [a] -> f [a]
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> t -> t -> f [a]
f t
t2 t
t1
splitfWithVariance t -> t -> f [a]
f t
t1 t
t2 Variance
Bivariant     = [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
(++) ([a] -> [a] -> [a]) -> f [a] -> f ([a] -> [a])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> t -> t -> f [a]
f t
t1 t
t2 f ([a] -> [a]) -> f [a] -> f [a]
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> t -> t -> f [a]
f t
t2 t
t1
splitfWithVariance t -> t -> f [a]
f t
t1 t
t2 Variance
Covariant     = t -> t -> f [a]
f t
t1 t
t2
splitfWithVariance t -> t -> f [a]
f t
t1 t
t2 Variance
Contravariant = t -> t -> f [a]
f t
t2 t
t1

updateEnv :: CGEnv -> RTVar RTyVar (RType RTyCon RTyVar b0) -> CG CGEnv
updateEnv :: forall b0.
CGEnv -> RTVar RTyVar (RType RTyCon RTyVar b0) -> CG CGEnv
updateEnv CGEnv
γ RTVar RTyVar (RType RTyCon RTyVar b0)
a
  | Just (Symbol
x, RType RTyCon RTyVar b0
s) <- RTVar RTyVar (RType RTyCon RTyVar b0)
-> Maybe (Symbol, RType RTyCon RTyVar b0)
forall s. RTVar RTyVar s -> Maybe (Symbol, s)
rTVarToBind RTVar RTyVar (RType RTyCon RTyVar b0)
a
  = CGEnv
γ CGEnv
-> ([Char], Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> CG CGEnv
+= ([Char]
"splitS RAllT", Symbol
x, (b0 -> RReft)
-> RType RTyCon RTyVar b0
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall a b.
(a -> b)
-> RTypeBV Symbol Symbol RTyCon RTyVar a
-> RTypeBV Symbol Symbol RTyCon RTyVar b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (RReft -> b0 -> RReft
forall a b. a -> b -> a
const RReft
forall a. Monoid a => a
mempty) RType RTyCon RTyVar b0
s)
  | Bool
otherwise
  = CGEnv -> CG CGEnv
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return CGEnv
γ

------------------------------------------------------------
splitC :: Bool -> SubC -> CG [FixSubC]
------------------------------------------------------------

splitC :: Bool -> SubC -> CG [FixSubC]
splitC Bool
allowTC (SubC CGEnv
γ (REx Symbol
x RTypeBV Symbol Symbol RTyCon RTyVar RReft
tx RTypeBV Symbol Symbol RTyCon RTyVar RReft
t1) (REx Symbol
x2 RTypeBV Symbol Symbol RTyCon RTyVar RReft
_ RTypeBV Symbol Symbol RTyCon RTyVar RReft
t2)) | Symbol
x Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
x2
  = do γ' <- CGEnv
γ CGEnv
-> ([Char], Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> CG CGEnv
+= ([Char]
"addExBind 0", Symbol
x, CGEnv
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forallExprRefType CGEnv
γ RTypeBV Symbol Symbol RTyCon RTyVar RReft
tx)
       splitC allowTC (SubC γ' t1 t2)

splitC Bool
allowTC (SubC CGEnv
γ RTypeBV Symbol Symbol RTyCon RTyVar RReft
t1 (REx Symbol
x RTypeBV Symbol Symbol RTyCon RTyVar RReft
tx RTypeBV Symbol Symbol RTyCon RTyVar RReft
t2))
  = do y <- StateT CGInfo Identity Symbol
forall (m :: * -> *) a. Freshable m a => m a
fresh
       γ' <- γ += ("addExBind 1", y, forallExprRefType γ tx)
       splitC allowTC (SubC γ' t1 (F.subst1 t2 (x, F.EVar y)))

-- existential at the left hand side is treated like forall
splitC Bool
allowTC (SubC CGEnv
γ (REx Symbol
x RTypeBV Symbol Symbol RTyCon RTyVar RReft
tx RTypeBV Symbol Symbol RTyCon RTyVar RReft
t1) RTypeBV Symbol Symbol RTyCon RTyVar RReft
t2)
  = do -- let tx' = traceShow ("splitC allowTC: " ++ showpp z) tx
       y <- StateT CGInfo Identity Symbol
forall (m :: * -> *) a. Freshable m a => m a
fresh
       γ' <- γ += ("addExBind 2", y, forallExprRefType γ tx)
       splitC allowTC (SubC γ' (F.subst1 t1 (x, F.EVar y)) t2)

splitC Bool
allowTC (SubC CGEnv
γ (RAllE Symbol
x RTypeBV Symbol Symbol RTyCon RTyVar RReft
tx RTypeBV Symbol Symbol RTyCon RTyVar RReft
t1) (RAllE Symbol
x2 RTypeBV Symbol Symbol RTyCon RTyVar RReft
_ RTypeBV Symbol Symbol RTyCon RTyVar RReft
t2)) | Symbol
x Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
x2
  = do γ' <- CGEnv
γ CGEnv
-> ([Char], Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> CG CGEnv
+= ([Char]
"addAllBind 3", Symbol
x, CGEnv
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forallExprRefType CGEnv
γ RTypeBV Symbol Symbol RTyCon RTyVar RReft
tx)
       splitC allowTC (SubC γ' t1 t2)

splitC Bool
allowTC (SubC CGEnv
γ (RAllE Symbol
x RTypeBV Symbol Symbol RTyCon RTyVar RReft
tx RTypeBV Symbol Symbol RTyCon RTyVar RReft
t1) RTypeBV Symbol Symbol RTyCon RTyVar RReft
t2)
  = do y  <- StateT CGInfo Identity Symbol
forall (m :: * -> *) a. Freshable m a => m a
fresh
       γ' <- γ += ("addAABind 1", y, forallExprRefType γ tx)
       splitC allowTC (SubC γ' (t1 `F.subst1` (x, F.EVar y)) t2)

splitC Bool
allowTC (SubC CGEnv
γ RTypeBV Symbol Symbol RTyCon RTyVar RReft
t1 (RAllE Symbol
x RTypeBV Symbol Symbol RTyCon RTyVar RReft
tx RTypeBV Symbol Symbol RTyCon RTyVar RReft
t2))
  = do y  <- StateT CGInfo Identity Symbol
forall (m :: * -> *) a. Freshable m a => m a
fresh
       γ' <- γ += ("addAllBind 2", y, forallExprRefType γ tx)
       splitC allowTC (SubC γ' t1 (F.subst1 t2 (x, F.EVar y)))

splitC Bool
allowTC (SubC CGEnv
cgenv (RRTy [(Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
env RReft
_ Oblig
OCons RTypeBV Symbol Symbol RTyCon RTyVar RReft
t1) RTypeBV Symbol Symbol RTyCon RTyVar RReft
t2)
  = do γ' <- (CGEnv
 -> (Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft) -> CG CGEnv)
-> CGEnv
-> [(Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
-> CG CGEnv
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\CGEnv
γ (Symbol
x, RTypeBV Symbol Symbol RTyCon RTyVar RReft
t) -> CGEnv
γ CGEnv
-> ([Char], Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> CG CGEnv
`addSEnv` ([Char]
"splitS", Symbol
x,RTypeBV Symbol Symbol RTyCon RTyVar RReft
t)) CGEnv
cgenv [(Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
xts
       c1 <- splitC allowTC (SubC γ' t1' t2')
       c2 <- splitC allowTC (SubC cgenv  t1  t2 )
       return $ c1 ++ c2
  where
    ([(Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
xts, RTypeBV Symbol Symbol RTyCon RTyVar RReft
t1', RTypeBV Symbol Symbol RTyCon RTyVar RReft
t2') = [(Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
-> ([(Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)],
    RTypeBV Symbol Symbol RTyCon RTyVar RReft,
    RTypeBV Symbol Symbol RTyCon RTyVar RReft)
forall a b. [(a, b)] -> ([(a, b)], b, b)
envToSub [(Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
env

splitC Bool
allowTC (SubC CGEnv
cgenv (RRTy [(Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
e RReft
r Oblig
o RTypeBV Symbol Symbol RTyCon RTyVar RReft
t1) RTypeBV Symbol Symbol RTyCon RTyVar RReft
t2)
  = do γ' <- (CGEnv
 -> (Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft) -> CG CGEnv)
-> CGEnv
-> [(Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
-> CG CGEnv
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\CGEnv
γ (Symbol
x, RTypeBV Symbol Symbol RTyCon RTyVar RReft
t) -> CGEnv
γ CGEnv
-> ([Char], Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> CG CGEnv
`addSEnv` ([Char]
"splitS", Symbol
x,RTypeBV Symbol Symbol RTyCon RTyVar RReft
t)) CGEnv
cgenv [(Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
e
       c1 <- splitC allowTC (SubR γ' o  r)
       c2 <- splitC allowTC (SubC cgenv t1 t2)
       return $ c1 ++ c2

splitC Bool
allowTC (SubC CGEnv
γ (RFun Symbol
x1 RFInfo
i1 RTypeBV Symbol Symbol RTyCon RTyVar RReft
t1 RTypeBV Symbol Symbol RTyCon RTyVar RReft
t1' RReft
r1) (RFun Symbol
x2 RFInfo
i2 RTypeBV Symbol Symbol RTyCon RTyVar RReft
t2 RTypeBV Symbol Symbol RTyCon RTyVar RReft
t2' RReft
r2))
  =  do cs'      <- Bool -> SubC -> CG [FixSubC]
splitC Bool
allowTC  (CGEnv
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> SubC
SubC CGEnv
γ RTypeBV Symbol Symbol RTyCon RTyVar RReft
t2 RTypeBV Symbol Symbol RTyCon RTyVar RReft
t1)
        γ'       <- γ+= ("splitC allowTC", x2, t2)
        cs       <- bsplitC γ (RFun x1 i1 t1 t1' (r1 `F.subst1` (x1, F.EVar x2)))
                              (RFun x2 i2 t2 t2'  r2)
        let t1x2' = RTypeBV Symbol Symbol RTyCon RTyVar RReft
t1' RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> (Variable (RTypeBV Symbol Symbol RTyCon RTyVar RReft),
    ExprBV
      (Variable (RTypeBV Symbol Symbol RTyCon RTyVar RReft))
      (Variable (RTypeBV Symbol Symbol RTyCon RTyVar RReft)))
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall a.
Subable a =>
a -> (Variable a, ExprBV (Variable a) (Variable a)) -> a
`F.subst1` (Symbol
Variable (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
x1, Symbol -> ExprBV Symbol Symbol
forall b v. v -> ExprBV b v
F.EVar Symbol
x2)
        cs''     <- splitC allowTC  (SubC γ' t1x2' t2')
        return    $ cs ++ cs' ++ cs''

splitC Bool
allowTC (SubC CGEnv
γ t1 :: RTypeBV Symbol Symbol RTyCon RTyVar RReft
t1@(RAppTy RTypeBV Symbol Symbol RTyCon RTyVar RReft
r1 RTypeBV Symbol Symbol RTyCon RTyVar RReft
r1' RReft
_) t2 :: RTypeBV Symbol Symbol RTyCon RTyVar RReft
t2@(RAppTy RTypeBV Symbol Symbol RTyCon RTyVar RReft
r2 RTypeBV Symbol Symbol RTyCon RTyVar RReft
r2' RReft
_))
  =  do cs    <- CGEnv
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> CG [FixSubC]
bsplitC CGEnv
γ RTypeBV Symbol Symbol RTyCon RTyVar RReft
t1 RTypeBV Symbol Symbol RTyCon RTyVar RReft
t2
        cs'   <- splitC allowTC  (SubC γ r1 r2)
        cs''  <- splitC allowTC  (SubC γ r1' r2')
        cs''' <- splitC allowTC  (SubC γ r2' r1')
        return $ cs ++ cs' ++ cs'' ++ cs'''

splitC Bool
allowTC (SubC CGEnv
γ RTypeBV Symbol Symbol RTyCon RTyVar RReft
t1 (RAllP PVUBV Symbol Symbol RTyCon RTyVar
p RTypeBV Symbol Symbol RTyCon RTyVar RReft
t))
  = Bool -> SubC -> CG [FixSubC]
splitC Bool
allowTC (SubC -> CG [FixSubC]) -> SubC -> CG [FixSubC]
forall a b. (a -> b) -> a -> b
$ CGEnv
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> SubC
SubC CGEnv
γ RTypeBV Symbol Symbol RTyCon RTyVar RReft
t1 RTypeBV Symbol Symbol RTyCon RTyVar RReft
t'
  where
    t' :: RTypeBV Symbol Symbol RTyCon RTyVar RReft
t' = (RReft -> RReft)
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall a b.
(a -> b)
-> RTypeBV Symbol Symbol RTyCon RTyVar a
-> RTypeBV Symbol Symbol RTyCon RTyVar b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((UsedPVar,
 (Symbol, [((), Symbol, ExprBV Symbol Symbol)])
 -> ExprBV Symbol Symbol)
-> RReft -> RReft
replacePredsWithRefs (UsedPVar,
 (Symbol, [((), Symbol, ExprBV Symbol Symbol)])
 -> ExprBV Symbol Symbol)
forall {a} {b}.
(UsedPVar,
 (Symbol, [(a, b, ExprBV Symbol Symbol)]) -> ExprBV Symbol Symbol)
su) RTypeBV Symbol Symbol RTyCon RTyVar RReft
t
    su :: (UsedPVar,
 (Symbol, [(a, b, ExprBV Symbol Symbol)]) -> ExprBV Symbol Symbol)
su = (PVUBV Symbol Symbol RTyCon RTyVar -> UsedPVar
forall v t. PVarV v t -> UsedPVarV v
uPVar PVUBV Symbol Symbol RTyCon RTyVar
p, PVUBV Symbol Symbol RTyCon RTyVar
-> (Symbol, [(a, b, ExprBV Symbol Symbol)]) -> ExprBV Symbol Symbol
forall t a b.
PVar t
-> (Symbol, [(a, b, ExprBV Symbol Symbol)]) -> ExprBV Symbol Symbol
pVartoRConc PVUBV Symbol Symbol RTyCon RTyVar
p)

splitC Bool
_ (SubC CGEnv
γ t1 :: RTypeBV Symbol Symbol RTyCon RTyVar RReft
t1@(RAllP PVUBV Symbol Symbol RTyCon RTyVar
_ RTypeBV Symbol Symbol RTyCon RTyVar RReft
_) RTypeBV Symbol Symbol RTyCon RTyVar RReft
t2)
  = Maybe SrcSpan -> [Char] -> CG [FixSubC]
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic (SrcSpan -> Maybe SrcSpan
forall a. a -> Maybe a
Just (SrcSpan -> Maybe SrcSpan) -> SrcSpan -> Maybe SrcSpan
forall a b. (a -> b) -> a -> b
$ CGEnv -> SrcSpan
getLocation CGEnv
γ) ([Char] -> CG [FixSubC]) -> [Char] -> CG [FixSubC]
forall a b. (a -> b) -> a -> b
$ [Char]
"Predicate in lhs of constraint:" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ RTypeBV Symbol Symbol RTyCon RTyVar RReft -> [Char]
forall a. PPrint a => a -> [Char]
showpp RTypeBV Symbol Symbol RTyCon RTyVar RReft
t1 [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n<:\n" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ RTypeBV Symbol Symbol RTyCon RTyVar RReft -> [Char]
forall a. PPrint a => a -> [Char]
showpp RTypeBV Symbol Symbol RTyCon RTyVar RReft
t2

splitC Bool
allowTC (SubC CGEnv
γ t1' :: RTypeBV Symbol Symbol RTyCon RTyVar RReft
t1'@(RAllT RTVar RTyVar (RType RTyCon RTyVar NoReft)
α1 RTypeBV Symbol Symbol RTyCon RTyVar RReft
t1 RReft
_) t2' :: RTypeBV Symbol Symbol RTyCon RTyVar RReft
t2'@(RAllT RTVar RTyVar (RType RTyCon RTyVar NoReft)
α2 RTypeBV Symbol Symbol RTyCon RTyVar RReft
t2 RReft
_))
  |  RTVar RTyVar (RType RTyCon RTyVar NoReft)
α1 RTVar RTyVar (RType RTyCon RTyVar NoReft)
-> RTVar RTyVar (RType RTyCon RTyVar NoReft) -> Bool
forall a. Eq a => a -> a -> Bool
==  RTVar RTyVar (RType RTyCon RTyVar NoReft)
α2
  = do γ'  <- CGEnv -> RTVar RTyVar (RType RTyCon RTyVar NoReft) -> CG CGEnv
forall b0.
CGEnv -> RTVar RTyVar (RType RTyCon RTyVar b0) -> CG CGEnv
updateEnv CGEnv
γ RTVar RTyVar (RType RTyCon RTyVar NoReft)
α2
       cs  <- bsplitC γ t1' t2'
       cs' <- splitC allowTC $ SubC γ' t1 (F.subst su t2)
       return (cs ++ cs')
  | Bool
otherwise
  = do γ'  <- CGEnv -> RTVar RTyVar (RType RTyCon RTyVar NoReft) -> CG CGEnv
forall b0.
CGEnv -> RTVar RTyVar (RType RTyCon RTyVar b0) -> CG CGEnv
updateEnv CGEnv
γ RTVar RTyVar (RType RTyCon RTyVar NoReft)
α2
       cs  <- bsplitC γ t1' t2'
       cs' <- splitC allowTC $ SubC γ' t1 (F.subst su t2'')
       return (cs ++ cs')
  where
    t2'' :: RTypeBV Symbol Symbol RTyCon RTyVar RReft
t2'' = (RTyVar, RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall tv r c b v.
(Eq tv, Hashable tv, IsReft r, TyConable c, Binder b,
 SubsTy tv (RTypeBV b v c tv (NoReftB b)) c,
 SubsTy tv (RTypeBV b v c tv (NoReftB b)) r,
 SubsTy
   tv (RTypeBV b v c tv (NoReftB b)) (RTypeBV b v c tv (NoReftB b)),
 FreeVar c tv, SubsTy tv (RTypeBV b v c tv (NoReftB b)) tv,
 SubsTy
   tv
   (RTypeBV b v c tv (NoReftB b))
   (RTVar tv (RTypeBV b v c tv (NoReftB b)))) =>
(tv, RTypeBV b v c tv r)
-> RTypeBV b v c tv r -> RTypeBV b v c tv r
subsTyVarMeet' (RTVar RTyVar (RType RTyCon RTyVar NoReft) -> RTyVar
forall tv s. RTVar tv s -> tv
ty_var_value RTVar RTyVar (RType RTyCon RTyVar NoReft)
α2, RTyVar -> RReft -> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall b v c tv r. tv -> r -> RTypeBV b v c tv r
RVar (RTVar RTyVar (RType RTyCon RTyVar NoReft) -> RTyVar
forall tv s. RTVar tv s -> tv
ty_var_value RTVar RTyVar (RType RTyCon RTyVar NoReft)
α1) RReft
forall a. Monoid a => a
mempty) RTypeBV Symbol Symbol RTyCon RTyVar RReft
t2
    su :: SubstV Symbol
su = case (RTVar RTyVar (RType RTyCon RTyVar NoReft)
-> Maybe (Symbol, RType RTyCon RTyVar NoReft)
forall s. RTVar RTyVar s -> Maybe (Symbol, s)
rTVarToBind RTVar RTyVar (RType RTyCon RTyVar NoReft)
α1, RTVar RTyVar (RType RTyCon RTyVar NoReft)
-> Maybe (Symbol, RType RTyCon RTyVar NoReft)
forall s. RTVar RTyVar s -> Maybe (Symbol, s)
rTVarToBind RTVar RTyVar (RType RTyCon RTyVar NoReft)
α2) of
          (Just (Symbol
x1, RType RTyCon RTyVar NoReft
_), Just (Symbol
x2, RType RTyCon RTyVar NoReft
_)) -> [(Symbol, ExprBV Symbol Symbol)] -> SubstV Symbol
forall v. Hashable v => [(v, ExprBV v v)] -> SubstV v
F.mkSubst [(Symbol
x1, Symbol -> ExprBV Symbol Symbol
forall b v. v -> ExprBV b v
F.EVar Symbol
x2)]
          (Maybe (Symbol, RType RTyCon RTyVar NoReft),
 Maybe (Symbol, RType RTyCon RTyVar NoReft))
_                            -> [(Symbol, ExprBV Symbol Symbol)] -> SubstV Symbol
forall v. Hashable v => [(v, ExprBV v v)] -> SubstV v
F.mkSubst []

splitC Bool
allowTC (SubC CGEnv
_ (RApp RTyCon
c1 [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
_ [RTPropBV Symbol Symbol RTyCon RTyVar RReft]
_ RReft
_) (RApp RTyCon
c2 [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
_ [RTPropBV Symbol Symbol RTyCon RTyVar RReft]
_ RReft
_)) | (if Bool
allowTC then RTyCon -> Bool
forall c. TyConable c => c -> Bool
isEmbeddedDict else RTyCon -> Bool
forall c. TyConable c => c -> Bool
isClass) RTyCon
c1 Bool -> Bool -> Bool
&& RTyCon
c1 RTyCon -> RTyCon -> Bool
forall a. Eq a => a -> a -> Bool
== RTyCon
c2
  = [FixSubC] -> CG [FixSubC]
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return []

splitC Bool
_ (SubC CGEnv
γ t1 :: RTypeBV Symbol Symbol RTyCon RTyVar RReft
t1@RApp{} t2 :: RTypeBV Symbol Symbol RTyCon RTyVar RReft
t2@RApp{})
  = do (t1',t2') <- RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> CG
     (RTypeBV Symbol Symbol RTyCon RTyVar RReft,
      RTypeBV Symbol Symbol RTyCon RTyVar RReft)
unifyVV RTypeBV Symbol Symbol RTyCon RTyVar RReft
t1 RTypeBV Symbol Symbol RTyCon RTyVar RReft
t2
       cs    <- bsplitC γ t1' t2'
       γ'    <- if bscope (getConfig γ) then γ `extendEnvWithVV` t1' else return γ
       let RApp c t1s r1s _ = t1'
       let RApp _ t2s r2s _ = t2'
       let isapplied = Bool
True -- TC.tyConArity (rtc_tc c) == length t1s
       let tyInfo = RTyCon -> TyConInfo
rtc_info RTyCon
c
       csvar  <-  splitsCWithVariance           γ' t1s t2s $ varianceTyArgs tyInfo
       csvar' <- rsplitsCWithVariance isapplied γ' r1s r2s $ variancePsArgs tyInfo
       return $ cs ++ csvar ++ csvar'

splitC Bool
_ (SubC CGEnv
γ t1 :: RTypeBV Symbol Symbol RTyCon RTyVar RReft
t1@(RVar RTyVar
a1 RReft
_) t2 :: RTypeBV Symbol Symbol RTyCon RTyVar RReft
t2@(RVar RTyVar
a2 RReft
_))
  | RTyVar
a1 RTyVar -> RTyVar -> Bool
forall a. Eq a => a -> a -> Bool
== RTyVar
a2
  = CGEnv
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> CG [FixSubC]
bsplitC CGEnv
γ RTypeBV Symbol Symbol RTyCon RTyVar RReft
t1 RTypeBV Symbol Symbol RTyCon RTyVar RReft
t2

splitC Bool
_ (SubC CGEnv
γ RTypeBV Symbol Symbol RTyCon RTyVar RReft
t1 RTypeBV Symbol Symbol RTyCon RTyVar RReft
t2)
  = Maybe SrcSpan -> [Char] -> CG [FixSubC]
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic (SrcSpan -> Maybe SrcSpan
forall a. a -> Maybe a
Just (SrcSpan -> Maybe SrcSpan) -> SrcSpan -> Maybe SrcSpan
forall a b. (a -> b) -> a -> b
$ CGEnv -> SrcSpan
getLocation CGEnv
γ) ([Char] -> CG [FixSubC]) -> [Char] -> CG [FixSubC]
forall a b. (a -> b) -> a -> b
$ [Char]
"(Another Broken Test!!!) splitc unexpected:\n" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ RTypeBV Symbol Symbol RTyCon RTyVar RReft -> [Char]
traceTy RTypeBV Symbol Symbol RTyCon RTyVar RReft
t1 [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n  <:\n" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ RTypeBV Symbol Symbol RTyCon RTyVar RReft -> [Char]
traceTy RTypeBV Symbol Symbol RTyCon RTyVar RReft
t2

splitC Bool
_ (SubR CGEnv
γ Oblig
o RReft
r)
  = do ts     <- CG Templates
getTemplates
       let r1' = SEnv Sort -> Templates -> SortedReft -> SortedReft
pruneUnsortedReft SEnv Sort
γ'' Templates
ts SortedReft
r1
       return $ F.subC γ' r1' r2 Nothing tag ci
  where
    γ'' :: SEnv Sort
γ'' = FEnv -> SEnv Sort
feEnv (FEnv -> SEnv Sort) -> FEnv -> SEnv Sort
forall a b. (a -> b) -> a -> b
$ CGEnv -> FEnv
fenv CGEnv
γ
    γ' :: IBindEnv
γ'  = FEnv -> IBindEnv
feBinds (FEnv -> IBindEnv) -> FEnv -> IBindEnv
forall a b. (a -> b) -> a -> b
$ CGEnv -> FEnv
fenv CGEnv
γ
    r1 :: SortedReft
r1  = Sort -> Reft -> SortedReft
F.RR Sort
F.boolSort Reft
rr
    r2 :: SortedReft
r2  = Sort -> Reft -> SortedReft
F.RR Sort
F.boolSort (Reft -> SortedReft) -> Reft -> SortedReft
forall a b. (a -> b) -> a -> b
$ (Symbol, ExprBV Symbol Symbol) -> Reft
forall b v. (b, ExprBV b v) -> ReftBV b v
F.Reft (Symbol
vv, Symbol -> ExprBV Symbol Symbol
forall b v. v -> ExprBV b v
F.EVar Symbol
vv)
    vv :: Symbol
vv  = Symbol
"vvRec"
    ci :: Cinfo
ci  = SrcSpan -> Maybe Error -> Maybe Var -> Cinfo
Ci SrcSpan
src Maybe Error
err (CGEnv -> Maybe Var
cgVar CGEnv
γ)
    err :: Maybe Error
err = Error -> Maybe Error
forall a. a -> Maybe a
Just (Error -> Maybe Error) -> Error -> Maybe Error
forall a b. (a -> b) -> a -> b
$ SrcSpan
-> Oblig
-> Doc
-> Maybe Integer
-> HashMap Symbol (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> Error
forall t.
SrcSpan
-> Oblig
-> Doc
-> Maybe Integer
-> HashMap Symbol t
-> t
-> TError t
ErrAssType SrcSpan
src Oblig
o ([Char] -> Doc
text ([Char] -> Doc) -> [Char] -> Doc
forall a b. (a -> b) -> a -> b
$ Oblig -> [Char]
forall a. Show a => a -> [Char]
show Oblig
o [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"type error") Maybe Integer
forall a. Maybe a
Nothing HashMap Symbol (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
g (Reft -> RTypeBV Symbol Symbol RTyCon RTyVar RReft
rHole Reft
rr)
    rr :: ReftBV (ReftBind RReft) (ReftVar RReft)
rr  = RReft -> ReftBV (ReftBind RReft) (ReftVar RReft)
forall r. ToReft r => r -> ReftBV (ReftBind r) (ReftVar r)
toReft RReft
r
    tag :: Tag
tag = CGEnv -> Tag
getTag CGEnv
γ
    src :: SrcSpan
src = CGEnv -> SrcSpan
getLocation CGEnv
γ
    g :: HashMap Symbol (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
g   = AREnv (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> HashMap Symbol (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
forall t. AREnv t -> HashMap Symbol t
reLocal (AREnv (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
 -> HashMap Symbol (RTypeBV Symbol Symbol RTyCon RTyVar RReft))
-> AREnv (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> HashMap Symbol (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
forall a b. (a -> b) -> a -> b
$ CGEnv -> AREnv (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
renv CGEnv
γ

traceTy :: SpecType -> String
traceTy :: RTypeBV Symbol Symbol RTyCon RTyVar RReft -> [Char]
traceTy (RVar RTyVar
v RReft
_)      = [Char] -> [Char]
parens ([Char]
"RVar " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ RTyVar -> [Char]
forall a. PPrint a => a -> [Char]
showpp RTyVar
v)
traceTy (RApp RTyCon
c [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
ts [RTPropBV Symbol Symbol RTyCon RTyVar RReft]
_ RReft
_) = [Char] -> [Char]
parens ([Char]
"RApp " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ RTyCon -> [Char]
forall a. PPrint a => a -> [Char]
showpp RTyCon
c [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [[Char]] -> [Char]
unwords (RTypeBV Symbol Symbol RTyCon RTyVar RReft -> [Char]
traceTy (RTypeBV Symbol Symbol RTyCon RTyVar RReft -> [Char])
-> [RTypeBV Symbol Symbol RTyCon RTyVar RReft] -> [[Char]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
ts))
traceTy (RAllP PVUBV Symbol Symbol RTyCon RTyVar
_ RTypeBV Symbol Symbol RTyCon RTyVar RReft
t)     = [Char] -> [Char]
parens ([Char]
"RAllP " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ RTypeBV Symbol Symbol RTyCon RTyVar RReft -> [Char]
traceTy RTypeBV Symbol Symbol RTyCon RTyVar RReft
t)
traceTy (RAllT RTVar RTyVar (RType RTyCon RTyVar NoReft)
_ RTypeBV Symbol Symbol RTyCon RTyVar RReft
t RReft
_)   = [Char] -> [Char]
parens ([Char]
"RAllT " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ RTypeBV Symbol Symbol RTyCon RTyVar RReft -> [Char]
traceTy RTypeBV Symbol Symbol RTyCon RTyVar RReft
t)
traceTy (RFun Symbol
_ RFInfo
_ RTypeBV Symbol Symbol RTyCon RTyVar RReft
t RTypeBV Symbol Symbol RTyCon RTyVar RReft
t' RReft
_) = [Char] -> [Char]
parens ([Char]
"RFun " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char] -> [Char]
parens (RTypeBV Symbol Symbol RTyCon RTyVar RReft -> [Char]
traceTy RTypeBV Symbol Symbol RTyCon RTyVar RReft
t) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char] -> [Char]
parens (RTypeBV Symbol Symbol RTyCon RTyVar RReft -> [Char]
traceTy RTypeBV Symbol Symbol RTyCon RTyVar RReft
t'))
traceTy (RAllE Symbol
_ RTypeBV Symbol Symbol RTyCon RTyVar RReft
tx RTypeBV Symbol Symbol RTyCon RTyVar RReft
t)  = [Char] -> [Char]
parens ([Char]
"RAllE " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char] -> [Char]
parens (RTypeBV Symbol Symbol RTyCon RTyVar RReft -> [Char]
traceTy RTypeBV Symbol Symbol RTyCon RTyVar RReft
tx) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char] -> [Char]
parens (RTypeBV Symbol Symbol RTyCon RTyVar RReft -> [Char]
traceTy RTypeBV Symbol Symbol RTyCon RTyVar RReft
t))
traceTy (REx Symbol
_ RTypeBV Symbol Symbol RTyCon RTyVar RReft
tx RTypeBV Symbol Symbol RTyCon RTyVar RReft
t)    = [Char] -> [Char]
parens ([Char]
"REx " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char] -> [Char]
parens (RTypeBV Symbol Symbol RTyCon RTyVar RReft -> [Char]
traceTy RTypeBV Symbol Symbol RTyCon RTyVar RReft
tx) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char] -> [Char]
parens (RTypeBV Symbol Symbol RTyCon RTyVar RReft -> [Char]
traceTy RTypeBV Symbol Symbol RTyCon RTyVar RReft
t))
traceTy (RExprArg Located (ExprBV Symbol Symbol)
_)    = [Char]
"RExprArg"
traceTy (RAppTy RTypeBV Symbol Symbol RTyCon RTyVar RReft
t RTypeBV Symbol Symbol RTyCon RTyVar RReft
t' RReft
_) = [Char] -> [Char]
parens ([Char]
"RAppTy " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char] -> [Char]
parens (RTypeBV Symbol Symbol RTyCon RTyVar RReft -> [Char]
traceTy RTypeBV Symbol Symbol RTyCon RTyVar RReft
t) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char] -> [Char]
parens (RTypeBV Symbol Symbol RTyCon RTyVar RReft -> [Char]
traceTy RTypeBV Symbol Symbol RTyCon RTyVar RReft
t'))
traceTy (RHole RReft
_)       = [Char]
"rHole"
traceTy (RRTy [(Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
_ RReft
_ Oblig
_ RTypeBV Symbol Symbol RTyCon RTyVar RReft
t)  = [Char] -> [Char]
parens ([Char]
"RRTy " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ RTypeBV Symbol Symbol RTyCon RTyVar RReft -> [Char]
traceTy RTypeBV Symbol Symbol RTyCon RTyVar RReft
t)

parens :: String -> String
parens :: [Char] -> [Char]
parens [Char]
s = [Char]
"(" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
s [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")"

rHole :: F.Reft -> SpecType
rHole :: Reft -> RTypeBV Symbol Symbol RTyCon RTyVar RReft
rHole = RReft -> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall b v c tv r. r -> RTypeBV b v c tv r
RHole (RReft -> RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> (Reft -> RReft)
-> Reft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Reft -> RReft
forall r v. r -> UReftV v r
uTop


splitsCWithVariance :: CGEnv
                    -> [SpecType]
                    -> [SpecType]
                    -> [Variance]
                    -> CG [FixSubC]
splitsCWithVariance :: CGEnv
-> [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
-> [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
-> [Variance]
-> CG [FixSubC]
splitsCWithVariance CGEnv
γ [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
t1s [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
t2s [Variance]
variants
  = ((RTypeBV Symbol Symbol RTyCon RTyVar RReft,
  RTypeBV Symbol Symbol RTyCon RTyVar RReft, Variance)
 -> CG [FixSubC])
-> [(RTypeBV Symbol Symbol RTyCon RTyVar RReft,
     RTypeBV Symbol Symbol RTyCon RTyVar RReft, Variance)]
-> CG [FixSubC]
forall (m :: * -> *) (t :: * -> *) a b.
(Monad m, Traversable t) =>
(a -> m [b]) -> t a -> m [b]
concatMapM (\(RTypeBV Symbol Symbol RTyCon RTyVar RReft
t1, RTypeBV Symbol Symbol RTyCon RTyVar RReft
t2, Variance
v) -> (RTypeBV Symbol Symbol RTyCon RTyVar RReft
 -> RTypeBV Symbol Symbol RTyCon RTyVar RReft -> CG [FixSubC])
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> Variance
-> CG [FixSubC]
forall (f :: * -> *) t a.
Applicative f =>
(t -> t -> f [a]) -> t -> t -> Variance -> f [a]
splitfWithVariance (\RTypeBV Symbol Symbol RTyCon RTyVar RReft
s1 RTypeBV Symbol Symbol RTyCon RTyVar RReft
s2 -> Bool -> SubC -> CG [FixSubC]
splitC (Config -> Bool
typeclass (CGEnv -> Config
forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)) (CGEnv
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> SubC
SubC CGEnv
γ RTypeBV Symbol Symbol RTyCon RTyVar RReft
s1 RTypeBV Symbol Symbol RTyCon RTyVar RReft
s2)) RTypeBV Symbol Symbol RTyCon RTyVar RReft
t1 RTypeBV Symbol Symbol RTyCon RTyVar RReft
t2 Variance
v) ([RTypeBV Symbol Symbol RTyCon RTyVar RReft]
-> [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
-> [Variance]
-> [(RTypeBV Symbol Symbol RTyCon RTyVar RReft,
     RTypeBV Symbol Symbol RTyCon RTyVar RReft, Variance)]
forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
zip3 [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
t1s [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
t2s [Variance]
variants)

rsplitsCWithVariance :: Bool
                     -> CGEnv
                     -> [SpecProp]
                     -> [SpecProp]
                     -> [Variance]
                     -> CG [FixSubC]
rsplitsCWithVariance :: Bool
-> CGEnv
-> [RTPropBV Symbol Symbol RTyCon RTyVar RReft]
-> [RTPropBV Symbol Symbol RTyCon RTyVar RReft]
-> [Variance]
-> CG [FixSubC]
rsplitsCWithVariance Bool
False CGEnv
_ [RTPropBV Symbol Symbol RTyCon RTyVar RReft]
_ [RTPropBV Symbol Symbol RTyCon RTyVar RReft]
_ [Variance]
_
  = [FixSubC] -> CG [FixSubC]
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return []

rsplitsCWithVariance Bool
_ CGEnv
γ [RTPropBV Symbol Symbol RTyCon RTyVar RReft]
t1s [RTPropBV Symbol Symbol RTyCon RTyVar RReft]
t2s [Variance]
variants
  = ((RTPropBV Symbol Symbol RTyCon RTyVar RReft,
  RTPropBV Symbol Symbol RTyCon RTyVar RReft, Variance)
 -> CG [FixSubC])
-> [(RTPropBV Symbol Symbol RTyCon RTyVar RReft,
     RTPropBV Symbol Symbol RTyCon RTyVar RReft, Variance)]
-> CG [FixSubC]
forall (m :: * -> *) (t :: * -> *) a b.
(Monad m, Traversable t) =>
(a -> m [b]) -> t a -> m [b]
concatMapM (\(RTPropBV Symbol Symbol RTyCon RTyVar RReft
t1, RTPropBV Symbol Symbol RTyCon RTyVar RReft
t2, Variance
v) -> (RTPropBV Symbol Symbol RTyCon RTyVar RReft
 -> RTPropBV Symbol Symbol RTyCon RTyVar RReft -> CG [FixSubC])
-> RTPropBV Symbol Symbol RTyCon RTyVar RReft
-> RTPropBV Symbol Symbol RTyCon RTyVar RReft
-> Variance
-> CG [FixSubC]
forall (f :: * -> *) t a.
Applicative f =>
(t -> t -> f [a]) -> t -> t -> Variance -> f [a]
splitfWithVariance (CGEnv
-> RTPropBV Symbol Symbol RTyCon RTyVar RReft
-> RTPropBV Symbol Symbol RTyCon RTyVar RReft
-> CG [FixSubC]
rsplitC CGEnv
γ) RTPropBV Symbol Symbol RTyCon RTyVar RReft
t1 RTPropBV Symbol Symbol RTyCon RTyVar RReft
t2 Variance
v) ([RTPropBV Symbol Symbol RTyCon RTyVar RReft]
-> [RTPropBV Symbol Symbol RTyCon RTyVar RReft]
-> [Variance]
-> [(RTPropBV Symbol Symbol RTyCon RTyVar RReft,
     RTPropBV Symbol Symbol RTyCon RTyVar RReft, Variance)]
forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
zip3 [RTPropBV Symbol Symbol RTyCon RTyVar RReft]
t1s [RTPropBV Symbol Symbol RTyCon RTyVar RReft]
t2s [Variance]
variants)

bsplitC :: CGEnv
        -> SpecType
        -> SpecType
        -> CG [F.SubC Cinfo]
bsplitC :: CGEnv
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> CG [FixSubC]
bsplitC CGEnv
γ RTypeBV Symbol Symbol RTyCon RTyVar RReft
t1 RTypeBV Symbol Symbol RTyCon RTyVar RReft
t2 = do
  temp   <- CG Templates
getTemplates
  isHO   <- gets allowHO
  t1'    <- addLhsInv γ <$> refreshVV t1
  return  $ bsplitC' γ t1' t2 temp isHO

addLhsInv :: CGEnv -> SpecType -> SpecType
addLhsInv :: CGEnv
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
addLhsInv CGEnv
γ RTypeBV Symbol Symbol RTyCon RTyVar RReft
t = RTyConInv
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
addRTyConInv (CGEnv -> RTyConInv
invs CGEnv
γ) RTypeBV Symbol Symbol RTyCon RTyVar RReft
t RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RReft -> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall r b v c tv.
Meet r =>
RTypeBV b v c tv r -> r -> RTypeBV b v c tv r
`strengthen` RReft
r
  where
    r :: RReft
r         = (RReft
forall a. Monoid a => a
mempty :: UReft F.Reft) { ur_reft = F.Reft (F.dummySymbol, p) }
    p :: ExprBV Symbol Symbol
p         = AREnv (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> LConstraint -> ExprBV Symbol Symbol
constraintToLogic AREnv (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
rE' (CGEnv -> LConstraint
lcs CGEnv
γ)
    rE' :: AREnv (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
rE'       = Symbol
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> AREnv (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> AREnv (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
insertREnv Symbol
v RTypeBV Symbol Symbol RTyCon RTyVar RReft
t (CGEnv -> AREnv (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
renv CGEnv
γ)
    v :: ReftBind RReft
v         = RTypeBV Symbol Symbol RTyCon RTyVar RReft -> ReftBind RReft
forall r b v c tv.
(ToReft r, Binder (ReftBind r)) =>
RTypeBV b v c tv r -> ReftBind r
rTypeValueVar RTypeBV Symbol Symbol RTyCon RTyVar RReft
t


bsplitC' :: CGEnv -> SpecType -> SpecType -> F.Templates -> Bool -> [F.SubC Cinfo]
bsplitC' :: CGEnv
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> Templates
-> Bool
-> [FixSubC]
bsplitC' CGEnv
γ RTypeBV Symbol Symbol RTyCon RTyVar RReft
t1 RTypeBV Symbol Symbol RTyCon RTyVar RReft
t2 Templates
tem Bool
isHO
 | Bool
isHO
 = IBindEnv
-> SortedReft
-> SortedReft
-> Tag
-> (SortedReft -> Cinfo)
-> [FixSubC]
forall a.
IBindEnv
-> SortedReft -> SortedReft -> Tag -> (SortedReft -> a) -> [SubC a]
mkSubC IBindEnv
γ' SortedReft
r1'  SortedReft
r2' Tag
tag SortedReft -> Cinfo
ci
 | SortedReft -> Bool
F.isFunctionSortedReft SortedReft
r1' Bool -> Bool -> Bool
&& SortedReft -> Bool
F.isNonTrivial SortedReft
r2'
 = IBindEnv
-> SortedReft
-> SortedReft
-> Tag
-> (SortedReft -> Cinfo)
-> [FixSubC]
forall a.
IBindEnv
-> SortedReft -> SortedReft -> Tag -> (SortedReft -> a) -> [SubC a]
mkSubC IBindEnv
γ' (SortedReft
r1' {F.sr_reft = mempty}) SortedReft
r2' Tag
tag SortedReft -> Cinfo
ci
 | SortedReft -> Bool
F.isNonTrivial SortedReft
r2'
 = IBindEnv
-> SortedReft
-> SortedReft
-> Tag
-> (SortedReft -> Cinfo)
-> [FixSubC]
forall a.
IBindEnv
-> SortedReft -> SortedReft -> Tag -> (SortedReft -> a) -> [SubC a]
mkSubC IBindEnv
γ' SortedReft
r1'  SortedReft
r2' Tag
tag SortedReft -> Cinfo
ci
 | Bool
otherwise
 = []
  where
    γ' :: IBindEnv
γ'  = FEnv -> IBindEnv
feBinds (FEnv -> IBindEnv) -> FEnv -> IBindEnv
forall a b. (a -> b) -> a -> b
$ CGEnv -> FEnv
fenv CGEnv
γ
    r1' :: SortedReft
r1' = CGEnv
-> Templates
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> SortedReft
forall r.
(PPrint r, IsReft r, ReftBind r ~ Symbol, ReftVar r ~ Symbol,
 SubsTy RTyVar (RType RTyCon RTyVar NoReft) r) =>
CGEnv -> Templates -> RRType r -> SortedReft
rTypeSortedReft' CGEnv
γ Templates
tem RTypeBV Symbol Symbol RTyCon RTyVar RReft
t1
    r2' :: SortedReft
r2' = CGEnv
-> Templates
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> SortedReft
forall r.
(PPrint r, IsReft r, ReftBind r ~ Symbol, ReftVar r ~ Symbol,
 SubsTy RTyVar (RType RTyCon RTyVar NoReft) r) =>
CGEnv -> Templates -> RRType r -> SortedReft
rTypeSortedReft' CGEnv
γ Templates
tem RTypeBV Symbol Symbol RTyCon RTyVar RReft
t2
    tag :: Tag
tag = CGEnv -> Tag
getTag CGEnv
γ
    src :: SrcSpan
src = CGEnv -> SrcSpan
getLocation CGEnv
γ
    g :: HashMap Symbol (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
g   = AREnv (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> HashMap Symbol (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
forall t. AREnv t -> HashMap Symbol t
reLocal (AREnv (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
 -> HashMap Symbol (RTypeBV Symbol Symbol RTyCon RTyVar RReft))
-> AREnv (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> HashMap Symbol (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
forall a b. (a -> b) -> a -> b
$ CGEnv -> AREnv (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
renv CGEnv
γ

    ci :: SortedReft -> Cinfo
ci SortedReft
sr  = SrcSpan -> Maybe Error -> Maybe Var -> Cinfo
Ci SrcSpan
src (SortedReft -> Maybe Error
err SortedReft
sr) (CGEnv -> Maybe Var
cgVar CGEnv
γ)
    err :: SortedReft -> Maybe Error
err SortedReft
sr = Error -> Maybe Error
forall a. a -> Maybe a
Just (Error -> Maybe Error) -> Error -> Maybe Error
forall a b. (a -> b) -> a -> b
$ Error -> Maybe Error -> Error
forall a. a -> Maybe a -> a
fromMaybe (SrcSpan
-> Doc
-> Maybe Integer
-> HashMap Symbol (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> Error
forall t.
SrcSpan
-> Doc -> Maybe Integer -> HashMap Symbol t -> t -> t -> TError t
ErrSubType SrcSpan
src ([Char] -> Doc
text [Char]
"subtype") Maybe Integer
forall a. Maybe a
Nothing HashMap Symbol (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
g RTypeBV Symbol Symbol RTyCon RTyVar RReft
t1 (RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> SortedReft -> RTypeBV Symbol Symbol RTyCon RTyVar RReft
replaceTop RTypeBV Symbol Symbol RTyCon RTyVar RReft
t2 SortedReft
sr)) (CGEnv -> Maybe Error
cerr CGEnv
γ)

mkSubC :: F.IBindEnv -> F.SortedReft -> F.SortedReft -> F.Tag -> (F.SortedReft -> a) -> [F.SubC a]
mkSubC :: forall a.
IBindEnv
-> SortedReft -> SortedReft -> Tag -> (SortedReft -> a) -> [SubC a]
mkSubC IBindEnv
g SortedReft
sr1 SortedReft
sr2 Tag
tag SortedReft -> a
ci = (SortedReft -> [SubC a]) -> [SortedReft] -> [SubC a]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\SortedReft
sr2' -> IBindEnv
-> SortedReft
-> SortedReft
-> Maybe Integer
-> Tag
-> a
-> [SubC a]
forall a.
IBindEnv
-> SortedReft
-> SortedReft
-> Maybe Integer
-> Tag
-> a
-> [SubC a]
F.subC IBindEnv
g SortedReft
sr1 SortedReft
sr2' Maybe Integer
forall a. Maybe a
Nothing Tag
tag (SortedReft -> a
ci SortedReft
sr2')) (SortedReft -> [SortedReft]
splitSortedReft SortedReft
sr2)

splitSortedReft :: F.SortedReft -> [F.SortedReft]
splitSortedReft :: SortedReft -> [SortedReft]
splitSortedReft (F.RR Sort
t (F.Reft (Symbol
v, ExprBV Symbol Symbol
r))) = [ Sort -> Reft -> SortedReft
F.RR Sort
t ((Symbol, ExprBV Symbol Symbol) -> Reft
forall b v. (b, ExprBV b v) -> ReftBV b v
F.Reft (Symbol
v, ExprBV Symbol Symbol
ra)) | ExprBV Symbol Symbol
ra <- ExprBV Symbol Symbol -> [ExprBV Symbol Symbol]
refaConjuncts ExprBV Symbol Symbol
r ]

refaConjuncts :: F.Expr -> [F.Expr]
refaConjuncts :: ExprBV Symbol Symbol -> [ExprBV Symbol Symbol]
refaConjuncts ExprBV Symbol Symbol
p = [ExprBV Symbol Symbol
p' | ExprBV Symbol Symbol
p' <- ExprBV Symbol Symbol -> [ExprBV Symbol Symbol]
forall b v. (Eq b, Eq v) => ExprBV b v -> [ExprBV b v]
F.conjuncts ExprBV Symbol Symbol
p, Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ ExprBV Symbol Symbol -> Bool
forall b v. (Eq b, Eq v) => ExprBV b v -> Bool
F.isTautoPred ExprBV Symbol Symbol
p']

replaceTop :: SpecType -> F.SortedReft -> SpecType
replaceTop :: RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> SortedReft -> RTypeBV Symbol Symbol RTyCon RTyVar RReft
replaceTop (RApp RTyCon
c [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
ts [RTPropBV Symbol Symbol RTyCon RTyVar RReft]
rs RReft
r) SortedReft
r'  = RTyCon
-> [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
-> [RTPropBV Symbol Symbol RTyCon RTyVar RReft]
-> RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall b v c tv r.
c
-> [RTypeBV b v c tv r]
-> [RTPropBV b v c tv r]
-> r
-> RTypeBV b v c tv r
RApp RTyCon
c [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
ts [RTPropBV Symbol Symbol RTyCon RTyVar RReft]
rs (RReft -> RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> RReft -> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall a b. (a -> b) -> a -> b
$ RReft -> SortedReft -> RReft
replaceReft RReft
r SortedReft
r'
replaceTop (RVar RTyVar
a RReft
r) SortedReft
r'        = RTyVar -> RReft -> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall b v c tv r. tv -> r -> RTypeBV b v c tv r
RVar RTyVar
a       (RReft -> RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> RReft -> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall a b. (a -> b) -> a -> b
$ RReft -> SortedReft -> RReft
replaceReft RReft
r SortedReft
r'
replaceTop (RFun Symbol
b RFInfo
i RTypeBV Symbol Symbol RTyCon RTyVar RReft
t1 RTypeBV Symbol Symbol RTyCon RTyVar RReft
t2 RReft
r) SortedReft
r' = Symbol
-> RFInfo
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall b v c tv r.
b
-> RFInfo
-> RTypeBV b v c tv r
-> RTypeBV b v c tv r
-> r
-> RTypeBV b v c tv r
RFun Symbol
b RFInfo
i RTypeBV Symbol Symbol RTyCon RTyVar RReft
t1 RTypeBV Symbol Symbol RTyCon RTyVar RReft
t2 (RReft -> RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> RReft -> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall a b. (a -> b) -> a -> b
$ RReft -> SortedReft -> RReft
replaceReft RReft
r SortedReft
r'
replaceTop (RAppTy RTypeBV Symbol Symbol RTyCon RTyVar RReft
t1 RTypeBV Symbol Symbol RTyCon RTyVar RReft
t2 RReft
r) SortedReft
r'  = RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall b v c tv r.
RTypeBV b v c tv r -> RTypeBV b v c tv r -> r -> RTypeBV b v c tv r
RAppTy RTypeBV Symbol Symbol RTyCon RTyVar RReft
t1 RTypeBV Symbol Symbol RTyCon RTyVar RReft
t2 (RReft -> RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> RReft -> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall a b. (a -> b) -> a -> b
$ RReft -> SortedReft -> RReft
replaceReft RReft
r SortedReft
r'
replaceTop (RAllT RTVar RTyVar (RType RTyCon RTyVar NoReft)
a RTypeBV Symbol Symbol RTyCon RTyVar RReft
t RReft
r)    SortedReft
r'  = RTVar RTyVar (RType RTyCon RTyVar NoReft)
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
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 RTVar RTyVar (RType RTyCon RTyVar NoReft)
a RTypeBV Symbol Symbol RTyCon RTyVar RReft
t    (RReft -> RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> RReft -> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall a b. (a -> b) -> a -> b
$ RReft -> SortedReft -> RReft
replaceReft RReft
r SortedReft
r'
replaceTop RTypeBV Symbol Symbol RTyCon RTyVar RReft
t SortedReft
_                  = RTypeBV Symbol Symbol RTyCon RTyVar RReft
t

replaceReft :: RReft -> F.SortedReft -> RReft
replaceReft :: RReft -> SortedReft -> RReft
replaceReft RReft
rr (F.RR Sort
_ Reft
r) = RReft
rr {ur_reft = F.Reft (v, F.subst1  p (vr, F.EVar v) )}
  where
    F.Reft (Symbol
v, ExprBV Symbol Symbol
_)         = RReft -> Reft
forall b v r. UReftBV b v r -> r
ur_reft RReft
rr
    F.Reft (Symbol
vr,ExprBV Symbol Symbol
p)         = Reft
r

unifyVV :: SpecType -> SpecType -> CG (SpecType, SpecType)
unifyVV :: RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> CG
     (RTypeBV Symbol Symbol RTyCon RTyVar RReft,
      RTypeBV Symbol Symbol RTyCon RTyVar RReft)
unifyVV t1 :: RTypeBV Symbol Symbol RTyCon RTyVar RReft
t1@RApp{} t2 :: RTypeBV Symbol Symbol RTyCon RTyVar RReft
t2@RApp{}
  = do vv <- 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)
-> StateT CGInfo Identity Integer -> StateT CGInfo Identity Symbol
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT CGInfo Identity Integer
forall (m :: * -> *) a. Freshable m a => m a
fresh
       return (shiftVV t1 vv, shiftVV t2 vv)

unifyVV RTypeBV Symbol Symbol RTyCon RTyVar RReft
_ RTypeBV Symbol Symbol RTyCon RTyVar RReft
_
  = Maybe SrcSpan
-> [Char]
-> CG
     (RTypeBV Symbol Symbol RTyCon RTyVar RReft,
      RTypeBV Symbol Symbol RTyCon RTyVar RReft)
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing [Char]
"Constraint.Generate.unifyVV called on invalid inputs"

rsplitC :: CGEnv
        -> SpecProp
        -> SpecProp
        -> CG [FixSubC]
rsplitC :: CGEnv
-> RTPropBV Symbol Symbol RTyCon RTyVar RReft
-> RTPropBV Symbol Symbol RTyCon RTyVar RReft
-> CG [FixSubC]
rsplitC CGEnv
_ RTPropBV Symbol Symbol RTyCon RTyVar RReft
_ (RProp [(Symbol, RType RTyCon RTyVar NoReft)]
_ (RHole RReft
_))
  = Maybe SrcSpan -> [Char] -> CG [FixSubC]
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing [Char]
"RefTypes.rsplitC on RProp _ (RHole _)"

rsplitC CGEnv
_ (RProp [(Symbol, RType RTyCon RTyVar NoReft)]
_ (RHole RReft
_)) RTPropBV Symbol Symbol RTyCon RTyVar RReft
_
  = Maybe SrcSpan -> [Char] -> CG [FixSubC]
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing [Char]
"RefTypes.rsplitC on RProp _ (RHole _)"

rsplitC CGEnv
γ (RProp [(Symbol, RType RTyCon RTyVar NoReft)]
s1 RTypeBV Symbol Symbol RTyCon RTyVar RReft
r1) (RProp [(Symbol, RType RTyCon RTyVar NoReft)]
s2 RTypeBV Symbol Symbol RTyCon RTyVar RReft
r2)
  = do γ'  <-  (CGEnv
 -> ([Char], Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)
 -> CG CGEnv)
-> CGEnv
-> [([Char], Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
-> CG CGEnv
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM CGEnv
-> ([Char], Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> CG CGEnv
(+=) CGEnv
γ [([Char]
"rsplitC1", Symbol
x, RType RTyCon RTyVar NoReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall r b v c tv.
IsReft r =>
RTypeBV b v c tv (NoReftB b) -> RTypeBV b v c tv r
ofRSort RType RTyCon RTyVar NoReft
s) | (Symbol
x, RType RTyCon RTyVar NoReft
s) <- [(Symbol, RType RTyCon RTyVar NoReft)]
s2]
       splitC (typeclass (getConfig γ)) (SubC γ' (F.subst su r1) r2)
  where su :: SubstV Symbol
su = [(Symbol, ExprBV Symbol Symbol)] -> SubstV Symbol
forall v. Hashable v => [(v, ExprBV v v)] -> SubstV v
F.mkSubst [(Symbol
x, Symbol -> ExprBV Symbol Symbol
forall b v. v -> ExprBV b v
F.EVar Symbol
y) | ((Symbol
x,RType RTyCon RTyVar NoReft
_), (Symbol
y,RType RTyCon RTyVar NoReft
_)) <- [(Symbol, RType RTyCon RTyVar NoReft)]
-> [(Symbol, RType RTyCon RTyVar NoReft)]
-> [((Symbol, RType RTyCon RTyVar NoReft),
     (Symbol, RType RTyCon RTyVar NoReft))]
forall a b. [a] -> [b] -> [(a, b)]
zip [(Symbol, RType RTyCon RTyVar NoReft)]
s1 [(Symbol, RType RTyCon RTyVar NoReft)]
s2]


--------------------------------------------------------------------------------
-- | Reftypes from F.Fixpoint Expressions --------------------------------------
--------------------------------------------------------------------------------
forallExprRefType     :: CGEnv -> SpecType -> SpecType
forallExprRefType :: CGEnv
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forallExprRefType CGEnv
γ RTypeBV Symbol Symbol RTyCon RTyVar RReft
t = RTypeBV Symbol Symbol RTyCon RTyVar RReft
t RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RReft -> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall r b v c tv.
Meet r =>
RTypeBV b v c tv r -> r -> RTypeBV b v c tv r
`strengthen` Reft -> RReft
forall r v. r -> UReftV v r
uTop Reft
r'
  where
    r' :: Reft
r'                = Reft -> Maybe Reft -> Reft
forall a. a -> Maybe a -> a
fromMaybe Reft
forall a. Monoid a => a
mempty (Maybe Reft -> Reft) -> Maybe Reft -> Reft
forall a b. (a -> b) -> a -> b
$ CGEnv -> Reft -> Maybe Reft
forallExprReft CGEnv
γ Reft
r
    r :: Reft
r                 = SortedReft -> Reft
F.sr_reft (SortedReft -> Reft) -> SortedReft -> Reft
forall a b. (a -> b) -> a -> b
$ TCEmb TyCon
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft -> SortedReft
forall r.
(PPrint r, IsReft r, ReftBind r ~ Symbol, ReftVar r ~ Symbol,
 SubsTy RTyVar (RType RTyCon RTyVar NoReft) r) =>
TCEmb TyCon -> RRType r -> SortedReft
rTypeSortedReft (CGEnv -> TCEmb TyCon
emb CGEnv
γ) RTypeBV Symbol Symbol RTyCon RTyVar RReft
t

forallExprReft :: CGEnv -> F.Reft -> Maybe F.Reft
forallExprReft :: CGEnv -> Reft -> Maybe Reft
forallExprReft CGEnv
γ Reft
r =
  do e <- Reft -> Maybe (ExprBV Symbol Symbol)
F.isSingletonReft Reft
r
     forallExprReft_ γ $ F.splitEApp e

forallExprReft_ :: CGEnv -> (F.Expr, [F.Expr]) -> Maybe F.Reft
forallExprReft_ :: CGEnv
-> (ExprBV Symbol Symbol, [ExprBV Symbol Symbol]) -> Maybe Reft
forallExprReft_ CGEnv
γ (F.EVar Symbol
x, [])
  = case CGEnv
-> Symbol
-> Maybe
     ([Symbol], [RFInfo], [RTypeBV Symbol Symbol RTyCon RTyVar RReft],
      [RReft], RTypeBV Symbol Symbol RTyCon RTyVar RReft)
forallExprReftLookup CGEnv
γ Symbol
x of
      Just ([Symbol]
_,[RFInfo]
_,[RTypeBV Symbol Symbol RTyCon RTyVar RReft]
_,[RReft]
_,RTypeBV Symbol Symbol RTyCon RTyVar RReft
t)  -> Reft -> Maybe Reft
forall a. a -> Maybe a
Just (Reft -> Maybe Reft) -> Reft -> Maybe Reft
forall a b. (a -> b) -> a -> b
$ SortedReft -> Reft
F.sr_reft (SortedReft -> Reft) -> SortedReft -> Reft
forall a b. (a -> b) -> a -> b
$ TCEmb TyCon
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft -> SortedReft
forall r.
(PPrint r, IsReft r, ReftBind r ~ Symbol, ReftVar r ~ Symbol,
 SubsTy RTyVar (RType RTyCon RTyVar NoReft) r) =>
TCEmb TyCon -> RRType r -> SortedReft
rTypeSortedReft (CGEnv -> TCEmb TyCon
emb CGEnv
γ) RTypeBV Symbol Symbol RTyCon RTyVar RReft
t
      Maybe
  ([Symbol], [RFInfo], [RTypeBV Symbol Symbol RTyCon RTyVar RReft],
   [RReft], RTypeBV Symbol Symbol RTyCon RTyVar RReft)
Nothing         -> Maybe Reft
forall a. Maybe a
Nothing

forallExprReft_ CGEnv
γ (F.EVar Symbol
f, [ExprBV Symbol Symbol]
es)
  = case CGEnv
-> Symbol
-> Maybe
     ([Symbol], [RFInfo], [RTypeBV Symbol Symbol RTyCon RTyVar RReft],
      [RReft], RTypeBV Symbol Symbol RTyCon RTyVar RReft)
forallExprReftLookup CGEnv
γ Symbol
f of
      Just ([Symbol]
xs,[RFInfo]
_,[RTypeBV Symbol Symbol RTyCon RTyVar RReft]
_,[RReft]
_,RTypeBV Symbol Symbol RTyCon RTyVar RReft
t) -> let su :: SubstV Symbol
su = [(Symbol, ExprBV Symbol Symbol)] -> SubstV Symbol
forall v. Hashable v => [(v, ExprBV v v)] -> SubstV v
F.mkSubst ([(Symbol, ExprBV Symbol Symbol)] -> SubstV Symbol)
-> [(Symbol, ExprBV Symbol Symbol)] -> SubstV Symbol
forall a b. (a -> b) -> a -> b
$ [Char]
-> [Symbol]
-> [ExprBV Symbol Symbol]
-> [(Symbol, ExprBV Symbol Symbol)]
forall a b. HasCallStack => [Char] -> [a] -> [b] -> [(a, b)]
safeZip [Char]
"fExprRefType" [Symbol]
xs [ExprBV Symbol Symbol]
es in
                       Reft -> Maybe Reft
forall a. a -> Maybe a
Just (Reft -> Maybe Reft) -> Reft -> Maybe Reft
forall a b. (a -> b) -> a -> b
$ SubstV (Variable Reft) -> Reft -> Reft
forall a.
(Subable a, HasCallStack) =>
SubstV (Variable a) -> a -> a
F.subst SubstV Symbol
SubstV (Variable Reft)
su (Reft -> Reft) -> Reft -> Reft
forall a b. (a -> b) -> a -> b
$ SortedReft -> Reft
F.sr_reft (SortedReft -> Reft) -> SortedReft -> Reft
forall a b. (a -> b) -> a -> b
$ TCEmb TyCon
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft -> SortedReft
forall r.
(PPrint r, IsReft r, ReftBind r ~ Symbol, ReftVar r ~ Symbol,
 SubsTy RTyVar (RType RTyCon RTyVar NoReft) r) =>
TCEmb TyCon -> RRType r -> SortedReft
rTypeSortedReft (CGEnv -> TCEmb TyCon
emb CGEnv
γ) RTypeBV Symbol Symbol RTyCon RTyVar RReft
t
      Maybe
  ([Symbol], [RFInfo], [RTypeBV Symbol Symbol RTyCon RTyVar RReft],
   [RReft], RTypeBV Symbol Symbol RTyCon RTyVar RReft)
Nothing       -> Maybe Reft
forall a. Maybe a
Nothing

forallExprReft_ CGEnv
_ (ExprBV Symbol Symbol, [ExprBV Symbol Symbol])
_
  = Maybe Reft
forall a. Maybe a
Nothing

-- forallExprReftLookup :: CGEnv -> F.Symbol -> Int
forallExprReftLookup :: CGEnv
                     -> F.Symbol
                     -> Maybe ([F.Symbol], [RFInfo], [SpecType], [RReft], SpecType)
forallExprReftLookup :: CGEnv
-> Symbol
-> Maybe
     ([Symbol], [RFInfo], [RTypeBV Symbol Symbol RTyCon RTyVar RReft],
      [RReft], RTypeBV Symbol Symbol RTyCon RTyVar RReft)
forallExprReftLookup CGEnv
γ Symbol
sym = RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> ([Symbol], [RFInfo],
    [RTypeBV Symbol Symbol RTyCon RTyVar RReft], [RReft],
    RTypeBV Symbol Symbol RTyCon RTyVar RReft)
forall {b} {v} {c} {tv} {r}.
RTypeBV b v c tv r
-> ([b], [RFInfo], [RTypeBV b v c tv r], [r], RTypeBV b v c tv r)
snap (RTypeBV Symbol Symbol RTyCon RTyVar RReft
 -> ([Symbol], [RFInfo],
     [RTypeBV Symbol Symbol RTyCon RTyVar RReft], [RReft],
     RTypeBV Symbol Symbol RTyCon RTyVar RReft))
-> Maybe (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> Maybe
     ([Symbol], [RFInfo], [RTypeBV Symbol Symbol RTyCon RTyVar RReft],
      [RReft], RTypeBV Symbol Symbol RTyCon RTyVar RReft)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Symbol -> Maybe (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
forall {a}.
Symbolic a =>
a -> Maybe (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
lookup' Symbol
sym
  where
    snap :: RTypeBV b v c tv r
-> ([b], [RFInfo], [RTypeBV b v c tv r], [r], RTypeBV b v c tv r)
snap     = (RTypeBV b v c tv r -> RTypeBV b v c tv r)
-> ([b], [RFInfo], [RTypeBV b v c tv r], [r], RTypeBV b v c tv r)
-> ([b], [RFInfo], [RTypeBV b v c tv r], [r], RTypeBV b v c tv r)
forall t t4 t0 t1 t2 t3.
(t -> t4) -> (t0, t1, t2, t3, t) -> (t0, t1, t2, t3, t4)
mapFifth5 RTypeBV b v c tv r -> RTypeBV b v c tv r
forall b v c tv r. RTypeBV b v c tv r -> RTypeBV b v c tv r
ignoreOblig (([b], [RFInfo], [RTypeBV b v c tv r], [r], RTypeBV b v c tv r)
 -> ([b], [RFInfo], [RTypeBV b v c tv r], [r], RTypeBV b v c tv r))
-> (RTypeBV b v c tv r
    -> ([b], [RFInfo], [RTypeBV b v c tv r], [r], RTypeBV b v c tv r))
-> RTypeBV b v c tv r
-> ([b], [RFInfo], [RTypeBV b v c tv r], [r], RTypeBV b v c tv r)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\(([b]
x,[RFInfo]
a,[RTypeBV b v c tv r]
b,[r]
c),RTypeBV b v c tv r
t)->([b]
x,[RFInfo]
a,[RTypeBV b v c tv r]
b,[r]
c,RTypeBV b v c tv r
t)) ((([b], [RFInfo], [RTypeBV b v c tv r], [r]), RTypeBV b v c tv r)
 -> ([b], [RFInfo], [RTypeBV b v c tv r], [r], RTypeBV b v c tv r))
-> (RTypeBV b v c tv r
    -> (([b], [RFInfo], [RTypeBV b v c tv r], [r]),
        RTypeBV b v c tv r))
-> RTypeBV b v c tv r
-> ([b], [RFInfo], [RTypeBV b v c tv r], [r], RTypeBV b v c tv r)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTypeBV b v c tv r
-> (([b], [RFInfo], [RTypeBV b v c tv r], [r]), RTypeBV b v c tv r)
forall b v t t1 a.
RTypeBV b v t t1 a
-> (([b], [RFInfo], [RTypeBV b v t t1 a], [a]), RTypeBV b v t t1 a)
bkArrow (RTypeBV b v c tv r
 -> (([b], [RFInfo], [RTypeBV b v c tv r], [r]),
     RTypeBV b v c tv r))
-> (RTypeBV b v c tv r -> RTypeBV b v c tv r)
-> RTypeBV b v c tv r
-> (([b], [RFInfo], [RTypeBV b v c tv r], [r]), RTypeBV b v c tv r)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([(RTVar tv (RTypeBV b v c tv (NoReftB b)), r)],
 [PVarBV b v (RTypeBV b v c tv (NoReftB b))], RTypeBV b v c tv r)
-> RTypeBV b v c tv r
forall a b c. (a, b, c) -> c
thd3 (([(RTVar tv (RTypeBV b v c tv (NoReftB b)), r)],
  [PVarBV b v (RTypeBV b v c tv (NoReftB b))], RTypeBV b v c tv r)
 -> RTypeBV b v c tv r)
-> (RTypeBV b v c tv r
    -> ([(RTVar tv (RTypeBV b v c tv (NoReftB b)), r)],
        [PVarBV b v (RTypeBV b v c tv (NoReftB b))], RTypeBV b v c tv r))
-> RTypeBV b v c tv r
-> RTypeBV b v c tv r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTypeBV b v c tv r
-> ([(RTVar tv (RTypeBV b v c tv (NoReftB b)), r)],
    [PVarBV b v (RTypeBV b v c tv (NoReftB b))], RTypeBV b v c tv r)
forall b v tv c r.
RTypeBV b v tv c r
-> ([(RTVar c (RTypeBV b v tv c (NoReftB b)), r)],
    [PVarBV b v (RTypeBV b v tv c (NoReftB b))], RTypeBV b v tv c r)
bkUniv
    lookup' :: a -> Maybe (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
lookup' a
z = CGEnv
γ HasCallStack =>
CGEnv
-> Symbol -> Maybe (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
CGEnv
-> Symbol -> Maybe (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
?= a -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol a
z


--------------------------------------------------------------------------------
getTag :: CGEnv -> F.Tag
--------------------------------------------------------------------------------
getTag :: CGEnv -> Tag
getTag CGEnv
γ = Tag -> (Var -> Tag) -> Maybe Var -> Tag
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Tag
Tg.defaultTag (Var -> TagEnv -> Tag
`Tg.getTag` CGEnv -> TagEnv
tgEnv CGEnv
γ) (CGEnv -> Maybe Var
tgKey CGEnv
γ)


--------------------------------------------------------------------------------
-- | Constraint Generation Panic -----------------------------------------------
--------------------------------------------------------------------------------
panicUnbound :: (PPrint x) => CGEnv -> x -> a
panicUnbound :: forall x a. PPrint x => CGEnv -> x -> a
panicUnbound CGEnv
γ x
x = Error -> a
forall a e. (HasCallStack, Exception e) => e -> a
Ex.throw (SrcSpan -> Doc -> Error
forall t. SrcSpan -> Doc -> TError t
ErrUnbound (CGEnv -> SrcSpan
getLocation CGEnv
γ) (x -> Doc
forall a. PPrint a => a -> Doc
F.pprint x
x) :: Error)