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

{-# 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 :: SpecType
t@(RFun Symbol
x RFInfo
_ SpecType
t1 SpecType
t2 RReft
_))
  =  do ws'  <- WfC -> CG [FixWfC]
splitW (CGEnv -> SpecType -> WfC
WfC CGEnv
γ SpecType
t1)
        γ'   <- γ += ("splitW", x, t1)
        ws   <- bsplitW γ t
        ws'' <- splitW (WfC γ' t2)
        return $ ws ++ ws' ++ ws''

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

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

splitW (WfC CGEnv
γ (RAllP PVUV Symbol RTyCon RTyVar
_ SpecType
r))
  = WfC -> CG [FixWfC]
splitW (CGEnv -> SpecType -> WfC
WfC CGEnv
γ SpecType
r)

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

splitW (WfC CGEnv
γ t :: SpecType
t@(RApp RTyCon
_ [SpecType]
ts [RTProp RTyCon RTyVar RReft]
rs RReft
_))
  =  do ws    <- CGEnv -> SpecType -> CG [FixWfC]
bsplitW CGEnv
γ SpecType
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 SpecType
tx SpecType
t))
  = do  ws  <- WfC -> CG [FixWfC]
splitW (CGEnv -> SpecType -> WfC
WfC CGEnv
γ SpecType
tx)
        γ'  <- γ += ("splitW1", x, tx)
        ws' <- splitW (WfC γ' t)
        return $ ws ++ ws'

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

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

splitW (WfC CGEnv
_ SpecType
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]
++ SpecType -> [Char]
forall a. PPrint a => a -> [Char]
showpp SpecType
t

rsplitW :: CGEnv
        -> Ref RSort SpecType
        -> CG [FixWfC]
rsplitW :: CGEnv -> RTProp RTyCon RTyVar RReft -> CG [FixWfC]
rsplitW CGEnv
_ (RProp [(Symbol, RType RTyCon RTyVar ())]
_ (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 ())]
ss SpecType
t0) = do
  γ' <- (CGEnv -> ([Char], Symbol, SpecType) -> CG CGEnv)
-> CGEnv -> [([Char], Symbol, SpecType)] -> CG CGEnv
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM CGEnv -> ([Char], Symbol, SpecType) -> CG CGEnv
(+=) CGEnv
γ [([Char]
"rsplitW", Symbol
x, RType RTyCon RTyVar () -> SpecType
forall r c tv. Reftable r => RType c tv () -> RType c tv r
ofRSort RType RTyCon RTyVar ()
s) | (Symbol
x, RType RTyCon RTyVar ()
s) <- [(Symbol, RType RTyCon RTyVar ())]
ss]
  splitW $ WfC γ' t0


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

bsplitW' :: (PPrint r, Reftable r, SubsTy RTyVar RSort r, Reftable (RTProp RTyCon RTyVar r))
         => CGEnv -> RRType r -> F.Templates -> Bool -> [F.WfC Cinfo]
bsplitW' :: forall r.
(PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r,
 Reftable (RTProp RTyCon RTyVar 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, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r,
 Reftable (RTProp RTyCon RTyVar 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, SpecType) -> CG CGEnv
+= ([Char]
"splitS RAllT", Symbol
x, (b0 -> RReft) -> RType RTyCon RTyVar b0 -> SpecType
forall a b.
(a -> b)
-> RTypeV Symbol RTyCon RTyVar a -> RTypeV 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 SpecType
tx SpecType
t1) (REx Symbol
x2 SpecType
_ SpecType
t2)) | Symbol
x Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
x2
  = do γ' <- CGEnv
γ CGEnv -> ([Char], Symbol, SpecType) -> CG CGEnv
+= ([Char]
"addExBind 0", Symbol
x, CGEnv -> SpecType -> SpecType
forallExprRefType CGEnv
γ SpecType
tx)
       splitC allowTC (SubC γ' t1 t2)

splitC Bool
allowTC (SubC CGEnv
γ SpecType
t1 (REx Symbol
x SpecType
tx SpecType
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 SpecType
tx SpecType
t1) SpecType
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 SpecType
tx SpecType
t1) (RAllE Symbol
x2 SpecType
_ SpecType
t2)) | Symbol
x Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
x2
  = do γ' <- CGEnv
γ CGEnv -> ([Char], Symbol, SpecType) -> CG CGEnv
+= ([Char]
"addAllBind 3", Symbol
x, CGEnv -> SpecType -> SpecType
forallExprRefType CGEnv
γ SpecType
tx)
       splitC allowTC (SubC γ' t1 t2)

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

splitC Bool
allowTC (SubC CGEnv
cgenv (RRTy [(Symbol, SpecType)]
e RReft
r Oblig
o SpecType
t1) SpecType
t2)
  = do γ' <- (CGEnv -> (Symbol, SpecType) -> CG CGEnv)
-> CGEnv -> [(Symbol, SpecType)] -> CG CGEnv
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\CGEnv
γ (Symbol
x, SpecType
t) -> CGEnv
γ CGEnv -> ([Char], Symbol, SpecType) -> CG CGEnv
`addSEnv` ([Char]
"splitS", Symbol
x,SpecType
t)) CGEnv
cgenv [(Symbol, SpecType)]
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 SpecType
t1 SpecType
t1' RReft
r1) (RFun Symbol
x2 RFInfo
i2 SpecType
t2 SpecType
t2' RReft
r2))
  =  do cs'      <- Bool -> SubC -> CG [FixSubC]
splitC Bool
allowTC  (CGEnv -> SpecType -> SpecType -> SubC
SubC CGEnv
γ SpecType
t2 SpecType
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' = SpecType
t1' SpecType -> (Symbol, ExprV Symbol) -> SpecType
forall a. Subable a => a -> (Symbol, ExprV Symbol) -> a
`F.subst1` (Symbol
x1, Symbol -> ExprV Symbol
forall v. v -> ExprV v
F.EVar Symbol
x2)
        cs''     <- splitC allowTC  (SubC γ' t1x2' t2')
        return    $ cs ++ cs' ++ cs''

splitC Bool
allowTC (SubC CGEnv
γ t1 :: SpecType
t1@(RAppTy SpecType
r1 SpecType
r1' RReft
_) t2 :: SpecType
t2@(RAppTy SpecType
r2 SpecType
r2' RReft
_))
  =  do cs    <- CGEnv -> SpecType -> SpecType -> CG [FixSubC]
bsplitC CGEnv
γ SpecType
t1 SpecType
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
γ SpecType
t1 (RAllP PVUV Symbol RTyCon RTyVar
p SpecType
t))
  = Bool -> SubC -> CG [FixSubC]
splitC Bool
allowTC (SubC -> CG [FixSubC]) -> SubC -> CG [FixSubC]
forall a b. (a -> b) -> a -> b
$ CGEnv -> SpecType -> SpecType -> SubC
SubC CGEnv
γ SpecType
t1 SpecType
t'
  where
    t' :: SpecType
t' = (RReft -> RReft) -> SpecType -> SpecType
forall a b.
(a -> b)
-> RTypeV Symbol RTyCon RTyVar a -> RTypeV Symbol RTyCon RTyVar b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((UsedPVar, (Symbol, [((), Symbol, ExprV Symbol)]) -> ExprV Symbol)
-> RReft -> RReft
replacePredsWithRefs (UsedPVar, (Symbol, [((), Symbol, ExprV Symbol)]) -> ExprV Symbol)
forall {a} {b}.
(UsedPVar, (Symbol, [(a, b, ExprV Symbol)]) -> ExprV Symbol)
su) SpecType
t
    su :: (UsedPVar, (Symbol, [(a, b, ExprV Symbol)]) -> ExprV Symbol)
su = (PVUV Symbol RTyCon RTyVar -> UsedPVar
forall v t. PVarV v t -> UsedPVarV v
uPVar PVUV Symbol RTyCon RTyVar
p, PVUV Symbol RTyCon RTyVar
-> (Symbol, [(a, b, ExprV Symbol)]) -> ExprV Symbol
forall t a b.
PVar t -> (Symbol, [(a, b, ExprV Symbol)]) -> ExprV Symbol
pVartoRConc PVUV Symbol RTyCon RTyVar
p)

splitC Bool
_ (SubC CGEnv
γ t1 :: SpecType
t1@(RAllP PVUV Symbol RTyCon RTyVar
_ SpecType
_) SpecType
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]
++ SpecType -> [Char]
forall a. PPrint a => a -> [Char]
showpp SpecType
t1 [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n<:\n" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SpecType -> [Char]
forall a. PPrint a => a -> [Char]
showpp SpecType
t2

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

splitC Bool
allowTC (SubC CGEnv
_ (RApp RTyCon
c1 [SpecType]
_ [RTProp RTyCon RTyVar RReft]
_ RReft
_) (RApp RTyCon
c2 [SpecType]
_ [RTProp 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 :: SpecType
t1@RApp{} t2 :: SpecType
t2@RApp{})
  = do (t1',t2') <- SpecType -> SpecType -> CG (SpecType, SpecType)
unifyVV SpecType
t1 SpecType
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 :: SpecType
t1@(RVar RTyVar
a1 RReft
_) t2 :: SpecType
t2@(RVar RTyVar
a2 RReft
_))
  | RTyVar
a1 RTyVar -> RTyVar -> Bool
forall a. Eq a => a -> a -> Bool
== RTyVar
a2
  = CGEnv -> SpecType -> SpecType -> CG [FixSubC]
bsplitC CGEnv
γ SpecType
t1 SpecType
t2

splitC Bool
_ (SubC CGEnv
γ SpecType
t1 SpecType
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]
++ SpecType -> [Char]
traceTy SpecType
t1 [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n  <:\n" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SpecType -> [Char]
traceTy SpecType
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, ExprV Symbol) -> Reft
forall v. (Symbol, ExprV v) -> ReftV v
F.Reft (Symbol
vv, Symbol -> ExprV Symbol
forall v. v -> ExprV 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 -> HashMap Symbol SpecType -> SpecType -> Error
forall t.
SrcSpan -> Oblig -> Doc -> 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") HashMap Symbol SpecType
g (Reft -> SpecType
rHole Reft
rr)
    rr :: Reft
rr  = RReft -> Reft
forall r. Reftable r => r -> Reft
toReft RReft
r
    tag :: Tag
tag = CGEnv -> Tag
getTag CGEnv
γ
    src :: SrcSpan
src = CGEnv -> SrcSpan
getLocation CGEnv
γ
    g :: HashMap Symbol SpecType
g   = AREnv SpecType -> HashMap Symbol SpecType
forall t. AREnv t -> HashMap Symbol t
reLocal (AREnv SpecType -> HashMap Symbol SpecType)
-> AREnv SpecType -> HashMap Symbol SpecType
forall a b. (a -> b) -> a -> b
$ CGEnv -> AREnv SpecType
renv CGEnv
γ

traceTy :: SpecType -> String
traceTy :: SpecType -> [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 [SpecType]
ts [RTProp 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 (SpecType -> [Char]
traceTy (SpecType -> [Char]) -> [SpecType] -> [[Char]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SpecType]
ts))
traceTy (RAllP PVUV Symbol RTyCon RTyVar
_ SpecType
t)     = [Char] -> [Char]
parens ([Char]
"RAllP " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SpecType -> [Char]
traceTy SpecType
t)
traceTy (RAllT RTVUV Symbol RTyCon RTyVar
_ SpecType
t RReft
_)   = [Char] -> [Char]
parens ([Char]
"RAllT " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SpecType -> [Char]
traceTy SpecType
t)
traceTy (RFun Symbol
_ RFInfo
_ SpecType
t SpecType
t' RReft
_) = [Char] -> [Char]
parens ([Char]
"RFun " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char] -> [Char]
parens (SpecType -> [Char]
traceTy SpecType
t) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char] -> [Char]
parens (SpecType -> [Char]
traceTy SpecType
t'))
traceTy (RAllE Symbol
_ SpecType
tx SpecType
t)  = [Char] -> [Char]
parens ([Char]
"RAllE " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char] -> [Char]
parens (SpecType -> [Char]
traceTy SpecType
tx) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char] -> [Char]
parens (SpecType -> [Char]
traceTy SpecType
t))
traceTy (REx Symbol
_ SpecType
tx SpecType
t)    = [Char] -> [Char]
parens ([Char]
"REx " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char] -> [Char]
parens (SpecType -> [Char]
traceTy SpecType
tx) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char] -> [Char]
parens (SpecType -> [Char]
traceTy SpecType
t))
traceTy (RExprArg Located (ExprV Symbol)
_)    = [Char]
"RExprArg"
traceTy (RAppTy SpecType
t SpecType
t' RReft
_) = [Char] -> [Char]
parens ([Char]
"RAppTy " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char] -> [Char]
parens (SpecType -> [Char]
traceTy SpecType
t) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char] -> [Char]
parens (SpecType -> [Char]
traceTy SpecType
t'))
traceTy (RHole RReft
_)       = [Char]
"rHole"
traceTy (RRTy [(Symbol, SpecType)]
_ RReft
_ Oblig
_ SpecType
t)  = [Char] -> [Char]
parens ([Char]
"RRTy " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SpecType -> [Char]
traceTy SpecType
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 -> SpecType
rHole = RReft -> SpecType
forall v c tv r. r -> RTypeV v c tv r
RHole (RReft -> SpecType) -> (Reft -> RReft) -> Reft -> SpecType
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 -> [SpecType] -> [SpecType] -> [Variance] -> CG [FixSubC]
splitsCWithVariance CGEnv
γ [SpecType]
t1s [SpecType]
t2s [Variance]
variants
  = ((SpecType, SpecType, Variance) -> CG [FixSubC])
-> [(SpecType, SpecType, Variance)] -> CG [FixSubC]
forall (m :: * -> *) (t :: * -> *) a b.
(Monad m, Traversable t) =>
(a -> m [b]) -> t a -> m [b]
concatMapM (\(SpecType
t1, SpecType
t2, Variance
v) -> (SpecType -> SpecType -> CG [FixSubC])
-> SpecType -> SpecType -> Variance -> CG [FixSubC]
forall (f :: * -> *) t a.
Applicative f =>
(t -> t -> f [a]) -> t -> t -> Variance -> f [a]
splitfWithVariance (\SpecType
s1 SpecType
s2 -> Bool -> SubC -> CG [FixSubC]
splitC (Config -> Bool
typeclass (CGEnv -> Config
forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)) (CGEnv -> SpecType -> SpecType -> SubC
SubC CGEnv
γ SpecType
s1 SpecType
s2)) SpecType
t1 SpecType
t2 Variance
v) ([SpecType]
-> [SpecType] -> [Variance] -> [(SpecType, SpecType, Variance)]
forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
zip3 [SpecType]
t1s [SpecType]
t2s [Variance]
variants)

rsplitsCWithVariance :: Bool
                     -> CGEnv
                     -> [SpecProp]
                     -> [SpecProp]
                     -> [Variance]
                     -> CG [FixSubC]
rsplitsCWithVariance :: Bool
-> CGEnv
-> [RTProp RTyCon RTyVar RReft]
-> [RTProp RTyCon RTyVar RReft]
-> [Variance]
-> CG [FixSubC]
rsplitsCWithVariance Bool
False CGEnv
_ [RTProp RTyCon RTyVar RReft]
_ [RTProp 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
γ [RTProp RTyCon RTyVar RReft]
t1s [RTProp RTyCon RTyVar RReft]
t2s [Variance]
variants
  = ((RTProp RTyCon RTyVar RReft, RTProp RTyCon RTyVar RReft, Variance)
 -> CG [FixSubC])
-> [(RTProp RTyCon RTyVar RReft, RTProp RTyCon RTyVar RReft,
     Variance)]
-> CG [FixSubC]
forall (m :: * -> *) (t :: * -> *) a b.
(Monad m, Traversable t) =>
(a -> m [b]) -> t a -> m [b]
concatMapM (\(RTProp RTyCon RTyVar RReft
t1, RTProp RTyCon RTyVar RReft
t2, Variance
v) -> (RTProp RTyCon RTyVar RReft
 -> RTProp RTyCon RTyVar RReft -> CG [FixSubC])
-> RTProp RTyCon RTyVar RReft
-> RTProp RTyCon RTyVar RReft
-> Variance
-> CG [FixSubC]
forall (f :: * -> *) t a.
Applicative f =>
(t -> t -> f [a]) -> t -> t -> Variance -> f [a]
splitfWithVariance (CGEnv
-> RTProp RTyCon RTyVar RReft
-> RTProp RTyCon RTyVar RReft
-> CG [FixSubC]
rsplitC CGEnv
γ) RTProp RTyCon RTyVar RReft
t1 RTProp RTyCon RTyVar RReft
t2 Variance
v) ([RTProp RTyCon RTyVar RReft]
-> [RTProp RTyCon RTyVar RReft]
-> [Variance]
-> [(RTProp RTyCon RTyVar RReft, RTProp RTyCon RTyVar RReft,
     Variance)]
forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
zip3 [RTProp RTyCon RTyVar RReft]
t1s [RTProp RTyCon RTyVar RReft]
t2s [Variance]
variants)

bsplitC :: CGEnv
        -> SpecType
        -> SpecType
        -> CG [F.SubC Cinfo]
bsplitC :: CGEnv -> SpecType -> SpecType -> CG [FixSubC]
bsplitC CGEnv
γ SpecType
t1 SpecType
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 -> SpecType -> SpecType
addLhsInv CGEnv
γ SpecType
t = RTyConInv -> SpecType -> SpecType
addRTyConInv (CGEnv -> RTyConInv
invs CGEnv
γ) SpecType
t SpecType -> RReft -> SpecType
forall r v c tv.
Reftable r =>
RTypeV v c tv r -> r -> RTypeV 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 :: ExprV Symbol
p         = AREnv SpecType -> LConstraint -> ExprV Symbol
constraintToLogic AREnv SpecType
rE' (CGEnv -> LConstraint
lcs CGEnv
γ)
    rE' :: AREnv SpecType
rE'       = Symbol -> SpecType -> AREnv SpecType -> AREnv SpecType
insertREnv Symbol
v SpecType
t (CGEnv -> AREnv SpecType
renv CGEnv
γ)
    v :: Symbol
v         = SpecType -> Symbol
forall r c tv. Reftable r => RType c tv r -> Symbol
rTypeValueVar SpecType
t


bsplitC' :: CGEnv -> SpecType -> SpecType -> F.Templates -> Bool -> [F.SubC Cinfo]
bsplitC' :: CGEnv -> SpecType -> SpecType -> Templates -> Bool -> [FixSubC]
bsplitC' CGEnv
γ SpecType
t1 SpecType
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 -> SpecType -> SortedReft
forall r.
(PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r,
 Reftable (RTProp RTyCon RTyVar r)) =>
CGEnv -> Templates -> RRType r -> SortedReft
rTypeSortedReft' CGEnv
γ Templates
tem SpecType
t1
    r2' :: SortedReft
r2' = CGEnv -> Templates -> SpecType -> SortedReft
forall r.
(PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r,
 Reftable (RTProp RTyCon RTyVar r)) =>
CGEnv -> Templates -> RRType r -> SortedReft
rTypeSortedReft' CGEnv
γ Templates
tem SpecType
t2
    tag :: Tag
tag = CGEnv -> Tag
getTag CGEnv
γ
    src :: SrcSpan
src = CGEnv -> SrcSpan
getLocation CGEnv
γ
    g :: HashMap Symbol SpecType
g   = AREnv SpecType -> HashMap Symbol SpecType
forall t. AREnv t -> HashMap Symbol t
reLocal (AREnv SpecType -> HashMap Symbol SpecType)
-> AREnv SpecType -> HashMap Symbol SpecType
forall a b. (a -> b) -> a -> b
$ CGEnv -> AREnv SpecType
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 SpecType
-> SpecType
-> SpecType
-> 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 SpecType
g SpecType
t1 (SpecType -> SortedReft -> SpecType
replaceTop SpecType
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, ExprV Symbol
r))) = [ Sort -> Reft -> SortedReft
F.RR Sort
t ((Symbol, ExprV Symbol) -> Reft
forall v. (Symbol, ExprV v) -> ReftV v
F.Reft (Symbol
v, ExprV Symbol
ra)) | ExprV Symbol
ra <- ExprV Symbol -> [ExprV Symbol]
refaConjuncts ExprV Symbol
r ]

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

replaceTop :: SpecType -> F.SortedReft -> SpecType
replaceTop :: SpecType -> SortedReft -> SpecType
replaceTop (RApp RTyCon
c [SpecType]
ts [RTProp RTyCon RTyVar RReft]
rs RReft
r) SortedReft
r'  = RTyCon
-> [SpecType] -> [RTProp RTyCon RTyVar RReft] -> RReft -> SpecType
forall v c tv r.
c
-> [RTypeV v c tv r] -> [RTPropV v c tv r] -> r -> RTypeV v c tv r
RApp RTyCon
c [SpecType]
ts [RTProp RTyCon RTyVar RReft]
rs (RReft -> SpecType) -> RReft -> SpecType
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 -> SpecType
forall v c tv r. tv -> r -> RTypeV v c tv r
RVar RTyVar
a       (RReft -> SpecType) -> RReft -> SpecType
forall a b. (a -> b) -> a -> b
$ RReft -> SortedReft -> RReft
replaceReft RReft
r SortedReft
r'
replaceTop (RFun Symbol
b RFInfo
i SpecType
t1 SpecType
t2 RReft
r) SortedReft
r' = Symbol -> RFInfo -> SpecType -> SpecType -> RReft -> SpecType
forall v c tv r.
Symbol
-> RFInfo
-> RTypeV v c tv r
-> RTypeV v c tv r
-> r
-> RTypeV v c tv r
RFun Symbol
b RFInfo
i SpecType
t1 SpecType
t2 (RReft -> SpecType) -> RReft -> SpecType
forall a b. (a -> b) -> a -> b
$ RReft -> SortedReft -> RReft
replaceReft RReft
r SortedReft
r'
replaceTop (RAppTy SpecType
t1 SpecType
t2 RReft
r) SortedReft
r'  = SpecType -> SpecType -> RReft -> SpecType
forall v c tv r.
RTypeV v c tv r -> RTypeV v c tv r -> r -> RTypeV v c tv r
RAppTy SpecType
t1 SpecType
t2 (RReft -> SpecType) -> RReft -> SpecType
forall a b. (a -> b) -> a -> b
$ RReft -> SortedReft -> RReft
replaceReft RReft
r SortedReft
r'
replaceTop (RAllT RTVUV Symbol RTyCon RTyVar
a SpecType
t RReft
r)    SortedReft
r'  = RTVUV Symbol RTyCon RTyVar -> SpecType -> RReft -> SpecType
forall v c tv r.
RTVUV v c tv -> RTypeV v c tv r -> r -> RTypeV v c tv r
RAllT RTVUV Symbol RTyCon RTyVar
a SpecType
t    (RReft -> SpecType) -> RReft -> SpecType
forall a b. (a -> b) -> a -> b
$ RReft -> SortedReft -> RReft
replaceReft RReft
r SortedReft
r'
replaceTop SpecType
t SortedReft
_                  = SpecType
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, ExprV Symbol
_)         = RReft -> Reft
forall v r. UReftV v r -> r
ur_reft RReft
rr
    F.Reft (Symbol
vr,ExprV Symbol
p)         = Reft
r

unifyVV :: SpecType -> SpecType -> CG (SpecType, SpecType)
unifyVV :: SpecType -> SpecType -> CG (SpecType, SpecType)
unifyVV t1 :: SpecType
t1@RApp{} t2 :: SpecType
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 SpecType
_ SpecType
_
  = Maybe SrcSpan -> [Char] -> CG (SpecType, SpecType)
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
-> RTProp RTyCon RTyVar RReft
-> RTProp RTyCon RTyVar RReft
-> CG [FixSubC]
rsplitC CGEnv
_ RTProp RTyCon RTyVar RReft
_ (RProp [(Symbol, RType RTyCon RTyVar ())]
_ (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 ())]
_ (RHole RReft
_)) RTProp 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 ())]
s1 SpecType
r1) (RProp [(Symbol, RType RTyCon RTyVar ())]
s2 SpecType
r2)
  = do γ'  <-  (CGEnv -> ([Char], Symbol, SpecType) -> CG CGEnv)
-> CGEnv -> [([Char], Symbol, SpecType)] -> CG CGEnv
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM CGEnv -> ([Char], Symbol, SpecType) -> CG CGEnv
(+=) CGEnv
γ [([Char]
"rsplitC1", Symbol
x, RType RTyCon RTyVar () -> SpecType
forall r c tv. Reftable r => RType c tv () -> RType c tv r
ofRSort RType RTyCon RTyVar ()
s) | (Symbol
x, RType RTyCon RTyVar ()
s) <- [(Symbol, RType RTyCon RTyVar ())]
s2]
       splitC (typeclass (getConfig γ)) (SubC γ' (F.subst su r1) r2)
  where su :: Subst
su = [(Symbol, ExprV Symbol)] -> Subst
F.mkSubst [(Symbol
x, Symbol -> ExprV Symbol
forall v. v -> ExprV v
F.EVar Symbol
y) | ((Symbol
x,RType RTyCon RTyVar ()
_), (Symbol
y,RType RTyCon RTyVar ()
_)) <- [(Symbol, RType RTyCon RTyVar ())]
-> [(Symbol, RType RTyCon RTyVar ())]
-> [((Symbol, RType RTyCon RTyVar ()),
     (Symbol, RType RTyCon RTyVar ()))]
forall a b. [a] -> [b] -> [(a, b)]
zip [(Symbol, RType RTyCon RTyVar ())]
s1 [(Symbol, RType RTyCon RTyVar ())]
s2]


--------------------------------------------------------------------------------
-- | Reftypes from F.Fixpoint Expressions --------------------------------------
--------------------------------------------------------------------------------
forallExprRefType     :: CGEnv -> SpecType -> SpecType
forallExprRefType :: CGEnv -> SpecType -> SpecType
forallExprRefType CGEnv
γ SpecType
t = SpecType
t SpecType -> RReft -> SpecType
forall r v c tv.
Reftable r =>
RTypeV v c tv r -> r -> RTypeV 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 -> SpecType -> SortedReft
forall r.
(PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r,
 Reftable (RTProp RTyCon RTyVar r)) =>
TCEmb TyCon -> RRType r -> SortedReft
rTypeSortedReft (CGEnv -> TCEmb TyCon
emb CGEnv
γ) SpecType
t

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

forallExprReft_ :: CGEnv -> (F.Expr, [F.Expr]) -> Maybe F.Reft
forallExprReft_ :: CGEnv -> (ExprV Symbol, [ExprV Symbol]) -> Maybe Reft
forallExprReft_ CGEnv
γ (F.EVar Symbol
x, [])
  = case CGEnv
-> Symbol
-> Maybe ([Symbol], [RFInfo], [SpecType], [RReft], SpecType)
forallExprReftLookup CGEnv
γ Symbol
x of
      Just ([Symbol]
_,[RFInfo]
_,[SpecType]
_,[RReft]
_,SpecType
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 -> SpecType -> SortedReft
forall r.
(PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r,
 Reftable (RTProp RTyCon RTyVar r)) =>
TCEmb TyCon -> RRType r -> SortedReft
rTypeSortedReft (CGEnv -> TCEmb TyCon
emb CGEnv
γ) SpecType
t
      Maybe ([Symbol], [RFInfo], [SpecType], [RReft], SpecType)
Nothing         -> Maybe Reft
forall a. Maybe a
Nothing

forallExprReft_ CGEnv
γ (F.EVar Symbol
f, [ExprV Symbol]
es)
  = case CGEnv
-> Symbol
-> Maybe ([Symbol], [RFInfo], [SpecType], [RReft], SpecType)
forallExprReftLookup CGEnv
γ Symbol
f of
      Just ([Symbol]
xs,[RFInfo]
_,[SpecType]
_,[RReft]
_,SpecType
t) -> let su :: Subst
su = [(Symbol, ExprV Symbol)] -> Subst
F.mkSubst ([(Symbol, ExprV Symbol)] -> Subst)
-> [(Symbol, ExprV Symbol)] -> Subst
forall a b. (a -> b) -> a -> b
$ [Char] -> [Symbol] -> [ExprV Symbol] -> [(Symbol, ExprV Symbol)]
forall a b. HasCallStack => [Char] -> [a] -> [b] -> [(a, b)]
safeZip [Char]
"fExprRefType" [Symbol]
xs [ExprV 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
$ Subst -> Reft -> Reft
forall a. Subable a => Subst -> a -> a
F.subst Subst
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 -> SpecType -> SortedReft
forall r.
(PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r,
 Reftable (RTProp RTyCon RTyVar r)) =>
TCEmb TyCon -> RRType r -> SortedReft
rTypeSortedReft (CGEnv -> TCEmb TyCon
emb CGEnv
γ) SpecType
t
      Maybe ([Symbol], [RFInfo], [SpecType], [RReft], SpecType)
Nothing       -> Maybe Reft
forall a. Maybe a
Nothing

forallExprReft_ CGEnv
_ (ExprV Symbol, [ExprV 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], [SpecType], [RReft], SpecType)
forallExprReftLookup CGEnv
γ Symbol
sym = SpecType -> ([Symbol], [RFInfo], [SpecType], [RReft], SpecType)
forall {t} {t1} {t2}.
RTypeV Symbol t t1 t2
-> ([Symbol], [RFInfo], [RTypeV Symbol t t1 t2], [t2],
    RTypeV Symbol t t1 t2)
snap (SpecType -> ([Symbol], [RFInfo], [SpecType], [RReft], SpecType))
-> Maybe SpecType
-> Maybe ([Symbol], [RFInfo], [SpecType], [RReft], SpecType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Symbol -> Maybe SpecType
forall {a}. Symbolic a => a -> Maybe SpecType
lookup' Symbol
sym
  where
    snap :: RTypeV Symbol t t1 t2
-> ([Symbol], [RFInfo], [RTypeV Symbol t t1 t2], [t2],
    RTypeV Symbol t t1 t2)
snap     = (RTypeV Symbol t t1 t2 -> RTypeV Symbol t t1 t2)
-> ([Symbol], [RFInfo], [RTypeV Symbol t t1 t2], [t2],
    RTypeV Symbol t t1 t2)
-> ([Symbol], [RFInfo], [RTypeV Symbol t t1 t2], [t2],
    RTypeV Symbol t t1 t2)
forall t t4 t0 t1 t2 t3.
(t -> t4) -> (t0, t1, t2, t3, t) -> (t0, t1, t2, t3, t4)
mapFifth5 RTypeV Symbol t t1 t2 -> RTypeV Symbol t t1 t2
forall t t1 t2. RType t t1 t2 -> RType t t1 t2
ignoreOblig (([Symbol], [RFInfo], [RTypeV Symbol t t1 t2], [t2],
  RTypeV Symbol t t1 t2)
 -> ([Symbol], [RFInfo], [RTypeV Symbol t t1 t2], [t2],
     RTypeV Symbol t t1 t2))
-> (RTypeV Symbol t t1 t2
    -> ([Symbol], [RFInfo], [RTypeV Symbol t t1 t2], [t2],
        RTypeV Symbol t t1 t2))
-> RTypeV Symbol t t1 t2
-> ([Symbol], [RFInfo], [RTypeV Symbol t t1 t2], [t2],
    RTypeV Symbol t t1 t2)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\(([Symbol]
x,[RFInfo]
a,[RTypeV Symbol t t1 t2]
b,[t2]
c),RTypeV Symbol t t1 t2
t)->([Symbol]
x,[RFInfo]
a,[RTypeV Symbol t t1 t2]
b,[t2]
c,RTypeV Symbol t t1 t2
t)) ((([Symbol], [RFInfo], [RTypeV Symbol t t1 t2], [t2]),
  RTypeV Symbol t t1 t2)
 -> ([Symbol], [RFInfo], [RTypeV Symbol t t1 t2], [t2],
     RTypeV Symbol t t1 t2))
-> (RTypeV Symbol t t1 t2
    -> (([Symbol], [RFInfo], [RTypeV Symbol t t1 t2], [t2]),
        RTypeV Symbol t t1 t2))
-> RTypeV Symbol t t1 t2
-> ([Symbol], [RFInfo], [RTypeV Symbol t t1 t2], [t2],
    RTypeV Symbol t t1 t2)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTypeV Symbol t t1 t2
-> (([Symbol], [RFInfo], [RTypeV Symbol t t1 t2], [t2]),
    RTypeV Symbol t t1 t2)
forall v t t1 a.
RTypeV v t t1 a
-> (([Symbol], [RFInfo], [RTypeV v t t1 a], [a]), RTypeV v t t1 a)
bkArrow (RTypeV Symbol t t1 t2
 -> (([Symbol], [RFInfo], [RTypeV Symbol t t1 t2], [t2]),
     RTypeV Symbol t t1 t2))
-> (RTypeV Symbol t t1 t2 -> RTypeV Symbol t t1 t2)
-> RTypeV Symbol t t1 t2
-> (([Symbol], [RFInfo], [RTypeV Symbol t t1 t2], [t2]),
    RTypeV Symbol t t1 t2)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([(RTVar t1 (RTypeV Symbol t t1 ()), t2)],
 [PVarV Symbol (RTypeV Symbol t t1 ())], RTypeV Symbol t t1 t2)
-> RTypeV Symbol t t1 t2
forall a b c. (a, b, c) -> c
thd3 (([(RTVar t1 (RTypeV Symbol t t1 ()), t2)],
  [PVarV Symbol (RTypeV Symbol t t1 ())], RTypeV Symbol t t1 t2)
 -> RTypeV Symbol t t1 t2)
-> (RTypeV Symbol t t1 t2
    -> ([(RTVar t1 (RTypeV Symbol t t1 ()), t2)],
        [PVarV Symbol (RTypeV Symbol t t1 ())], RTypeV Symbol t t1 t2))
-> RTypeV Symbol t t1 t2
-> RTypeV Symbol t t1 t2
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTypeV Symbol t t1 t2
-> ([(RTVar t1 (RTypeV Symbol t t1 ()), t2)],
    [PVarV Symbol (RTypeV Symbol t t1 ())], RTypeV Symbol t t1 t2)
forall v tv c r.
RTypeV v tv c r
-> ([(RTVar c (RTypeV v tv c ()), r)],
    [PVarV v (RTypeV v tv c ())], RTypeV v tv c r)
bkUniv
    lookup' :: a -> Maybe SpecType
lookup' a
z = CGEnv
γ HasCallStack => CGEnv -> Symbol -> Maybe SpecType
CGEnv -> Symbol -> Maybe SpecType
?= 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)