{-# 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 hiding (loc)


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 [FixWfC]
ws'  <- WfC -> CG [FixWfC]
splitW (CGEnv -> SpecType -> WfC
WfC CGEnv
γ SpecType
t1)
        CGEnv
γ'   <- CGEnv
γ CGEnv -> ([Char], Symbol, SpecType) -> CG CGEnv
+= ([Char]
"splitW", Symbol
x, SpecType
t1)
        [FixWfC]
ws   <- CGEnv -> SpecType -> CG [FixWfC]
bsplitW CGEnv
γ SpecType
t
        [FixWfC]
ws'' <- WfC -> CG [FixWfC]
splitW (CGEnv -> SpecType -> WfC
WfC CGEnv
γ' SpecType
t2)
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [FixWfC]
ws forall a. [a] -> [a] -> [a]
++ [FixWfC]
ws' forall a. [a] -> [a] -> [a]
++ [FixWfC]
ws''

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

splitW (WfC CGEnv
γ t' :: SpecType
t'@(RAllT RTVU RTyCon RTyVar
a SpecType
t RReft
_))
  = do CGEnv
γ'  <- forall b0.
CGEnv -> RTVar RTyVar (RType RTyCon RTyVar b0) -> CG CGEnv
updateEnv CGEnv
γ RTVU RTyCon RTyVar
a
       [FixWfC]
ws  <- CGEnv -> SpecType -> CG [FixWfC]
bsplitW CGEnv
γ SpecType
t'
       [FixWfC]
ws' <- WfC -> CG [FixWfC]
splitW (CGEnv -> SpecType -> WfC
WfC CGEnv
γ' SpecType
t)
       forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [FixWfC]
ws forall a. [a] -> [a] -> [a]
++ [FixWfC]
ws'

splitW (WfC CGEnv
γ (RAllP PVU 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 [FixWfC]
ws    <- CGEnv -> SpecType -> CG [FixWfC]
bsplitW CGEnv
γ SpecType
t
        CGEnv
γ'    <- if Config -> Bool
bscope (forall t. HasConfig t => t -> Config
getConfig CGEnv
γ) then CGEnv
γ CGEnv -> SpecType -> CG CGEnv
`extendEnvWithVV` SpecType
t else forall (m :: * -> *) a. Monad m => a -> m a
return CGEnv
γ
        [FixWfC]
ws'   <- forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (WfC -> CG [FixWfC]
splitW forall b c a. (b -> c) -> (a -> b) -> a -> c
. CGEnv -> SpecType -> WfC
WfC CGEnv
γ') [SpecType]
ts
        [FixWfC]
ws''  <- forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (CGEnv -> RTProp RTyCon RTyVar RReft -> CG [FixWfC]
rsplitW CGEnv
γ)       [RTProp RTyCon RTyVar RReft]
rs
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [FixWfC]
ws forall a. [a] -> [a] -> [a]
++ [FixWfC]
ws' forall a. [a] -> [a] -> [a]
++ [FixWfC]
ws''

splitW (WfC CGEnv
γ (RAllE Symbol
x SpecType
tx SpecType
t))
  = do  [FixWfC]
ws  <- WfC -> CG [FixWfC]
splitW (CGEnv -> SpecType -> WfC
WfC CGEnv
γ SpecType
tx)
        CGEnv
γ'  <- CGEnv
γ CGEnv -> ([Char], Symbol, SpecType) -> CG CGEnv
+= ([Char]
"splitW1", Symbol
x, SpecType
tx)
        [FixWfC]
ws' <- WfC -> CG [FixWfC]
splitW (CGEnv -> SpecType -> WfC
WfC CGEnv
γ' SpecType
t)
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [FixWfC]
ws forall a. [a] -> [a] -> [a]
++ [FixWfC]
ws'

splitW (WfC CGEnv
γ (REx Symbol
x SpecType
tx SpecType
t))
  = do  [FixWfC]
ws  <- WfC -> CG [FixWfC]
splitW (CGEnv -> SpecType -> WfC
WfC CGEnv
γ SpecType
tx)
        CGEnv
γ'  <- CGEnv
γ CGEnv -> ([Char], Symbol, SpecType) -> CG CGEnv
+= ([Char]
"splitW2", Symbol
x, SpecType
tx)
        [FixWfC]
ws' <- WfC -> CG [FixWfC]
splitW (CGEnv -> SpecType -> WfC
WfC CGEnv
γ' SpecType
t)
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [FixWfC]
ws forall a. [a] -> [a] -> [a]
++ [FixWfC]
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)
  = forall a. Maybe SrcSpan -> [Char] -> a
panic forall a. Maybe a
Nothing forall a b. (a -> b) -> a -> b
$ [Char]
"splitW cannot handle: " forall a. [a] -> [a] -> [a]
++ 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
_)) =
  forall a. Maybe SrcSpan -> [Char] -> a
panic forall a. Maybe a
Nothing [Char]
"Constrains: rsplitW for RProp _ (RHole _)"

rsplitW CGEnv
γ (RProp [(Symbol, RType RTyCon RTyVar ())]
ss SpecType
t0) = do
  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, 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]
  WfC -> CG [FixWfC]
splitW forall a b. (a -> b) -> a -> b
$ CGEnv -> SpecType -> WfC
WfC CGEnv
γ' SpecType
t0


bsplitW :: CGEnv -> SpecType -> CG [FixWfC]
bsplitW :: CGEnv -> SpecType -> CG [FixWfC]
bsplitW CGEnv
γ SpecType
t =
  do Templates
temp  <- CG Templates
getTemplates
     Bool
isHO  <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CGInfo -> Bool
allowHO
     forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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
γ SpecType
t Templates
temp Bool
isHO

bsplitW' :: (PPrint r, F.Reftable r, SubsTy RTyVar RSort r, F.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
|| forall r. Reftable r => r -> Bool
F.isNonTrivial SortedReft
r'
  = forall a. Fixpoint a => IBindEnv -> SortedReft -> a -> [WfC a]
F.wfC (FEnv -> IBindEnv
feBinds forall a b. (a -> b) -> a -> b
$ CGEnv -> FEnv
fenv CGEnv
γ) SortedReft
r' Cinfo
ci
  | Bool
otherwise
  = []
  where
    r' :: SortedReft
r'                = 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
γ) 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     = forall a. [a] -> [a] -> [a]
(++) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> t -> t -> f [a]
f t
t1 t
t2 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     = forall a. [a] -> [a] -> [a]
(++) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> t -> t -> f [a]
f t
t1 t
t2 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) <- 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, forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a b. a -> b -> a
const forall a. Monoid a => a
mempty) RType RTyCon RTyVar b0
s)
  | Bool
otherwise
  = 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 forall a. Eq a => a -> a -> Bool
== Symbol
x2
  = do CGEnv
γ' <- CGEnv
γ CGEnv -> ([Char], Symbol, SpecType) -> CG CGEnv
+= ([Char]
"addExBind 0", Symbol
x, CGEnv -> SpecType -> SpecType
forallExprRefType CGEnv
γ SpecType
tx)
       Bool -> SubC -> CG [FixSubC]
splitC Bool
allowTC (CGEnv -> SpecType -> SpecType -> SubC
SubC CGEnv
γ' SpecType
t1 SpecType
t2)

splitC Bool
allowTC (SubC CGEnv
γ SpecType
t1 (REx Symbol
x SpecType
tx SpecType
t2))
  = do Symbol
y <- forall (m :: * -> *) a. Freshable m a => m a
fresh
       CGEnv
γ' <- CGEnv
γ CGEnv -> ([Char], Symbol, SpecType) -> CG CGEnv
+= ([Char]
"addExBind 1", Symbol
y, CGEnv -> SpecType -> SpecType
forallExprRefType CGEnv
γ SpecType
tx)
       Bool -> SubC -> CG [FixSubC]
splitC Bool
allowTC (CGEnv -> SpecType -> SpecType -> SubC
SubC CGEnv
γ' SpecType
t1 (forall a. Subable a => a -> (Symbol, Expr) -> a
F.subst1 SpecType
t2 (Symbol
x, Symbol -> Expr
F.EVar Symbol
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
       Symbol
y <- forall (m :: * -> *) a. Freshable m a => m a
fresh
       CGEnv
γ' <- CGEnv
γ CGEnv -> ([Char], Symbol, SpecType) -> CG CGEnv
+= ([Char]
"addExBind 2", Symbol
y, CGEnv -> SpecType -> SpecType
forallExprRefType CGEnv
γ SpecType
tx)
       Bool -> SubC -> CG [FixSubC]
splitC Bool
allowTC (CGEnv -> SpecType -> SpecType -> SubC
SubC CGEnv
γ' (forall a. Subable a => a -> (Symbol, Expr) -> a
F.subst1 SpecType
t1 (Symbol
x, Symbol -> Expr
F.EVar Symbol
y)) SpecType
t2)

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

splitC Bool
allowTC (SubC CGEnv
γ (RAllE Symbol
x SpecType
tx SpecType
t1) SpecType
t2)
  = do Symbol
y  <- forall (m :: * -> *) a. Freshable m a => m a
fresh
       CGEnv
γ' <- CGEnv
γ CGEnv -> ([Char], Symbol, SpecType) -> CG CGEnv
+= ([Char]
"addAABind 1", Symbol
y, CGEnv -> SpecType -> SpecType
forallExprRefType CGEnv
γ SpecType
tx)
       Bool -> SubC -> CG [FixSubC]
splitC Bool
allowTC (CGEnv -> SpecType -> SpecType -> SubC
SubC CGEnv
γ' (SpecType
t1 forall a. Subable a => a -> (Symbol, Expr) -> a
`F.subst1` (Symbol
x, Symbol -> Expr
F.EVar Symbol
y)) SpecType
t2)

splitC Bool
allowTC (SubC CGEnv
γ SpecType
t1 (RAllE Symbol
x SpecType
tx SpecType
t2))
  = do Symbol
y  <- forall (m :: * -> *) a. Freshable m a => m a
fresh
       CGEnv
γ' <- CGEnv
γ CGEnv -> ([Char], Symbol, SpecType) -> CG CGEnv
+= ([Char]
"addAllBind 2", Symbol
y, CGEnv -> SpecType -> SpecType
forallExprRefType CGEnv
γ SpecType
tx)
       Bool -> SubC -> CG [FixSubC]
splitC Bool
allowTC (CGEnv -> SpecType -> SpecType -> SubC
SubC CGEnv
γ' SpecType
t1 (forall a. Subable a => a -> (Symbol, Expr) -> a
F.subst1 SpecType
t2 (Symbol
x, Symbol -> Expr
F.EVar Symbol
y)))

splitC Bool
allowTC (SubC CGEnv
cgenv (RRTy [(Symbol, SpecType)]
env RReft
_ Oblig
OCons SpecType
t1) SpecType
t2)
  = do 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
       [FixSubC]
c1 <- Bool -> SubC -> CG [FixSubC]
splitC Bool
allowTC (CGEnv -> SpecType -> SpecType -> SubC
SubC CGEnv
γ' SpecType
t1' SpecType
t2')
       [FixSubC]
c2 <- Bool -> SubC -> CG [FixSubC]
splitC Bool
allowTC (CGEnv -> SpecType -> SpecType -> SubC
SubC CGEnv
cgenv  SpecType
t1  SpecType
t2 )
       forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [FixSubC]
c1 forall a. [a] -> [a] -> [a]
++ [FixSubC]
c2
  where
    ([(Symbol, SpecType)]
xts, SpecType
t1', SpecType
t2') = 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
γ' <- 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
       [FixSubC]
c1 <- Bool -> SubC -> CG [FixSubC]
splitC Bool
allowTC (CGEnv -> Oblig -> RReft -> SubC
SubR CGEnv
γ' Oblig
o  RReft
r)
       [FixSubC]
c2 <- Bool -> SubC -> CG [FixSubC]
splitC Bool
allowTC (CGEnv -> SpecType -> SpecType -> SubC
SubC CGEnv
cgenv SpecType
t1 SpecType
t2)
       forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [FixSubC]
c1 forall a. [a] -> [a] -> [a]
++ [FixSubC]
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 [FixSubC]
cs'      <- Bool -> SubC -> CG [FixSubC]
splitC Bool
allowTC  (CGEnv -> SpecType -> SpecType -> SubC
SubC CGEnv
γ SpecType
t2 SpecType
t1)
        CGEnv
γ'       <- CGEnv
γCGEnv -> ([Char], Symbol, SpecType) -> CG CGEnv
+= ([Char]
"splitC allowTC", Symbol
x2, SpecType
t2)
        [FixSubC]
cs       <- CGEnv -> SpecType -> SpecType -> CG [FixSubC]
bsplitC CGEnv
γ (forall c tv r.
Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
x1 RFInfo
i1 SpecType
t1 SpecType
t1' (RReft
r1 forall a. Subable a => a -> (Symbol, Expr) -> a
`F.subst1` (Symbol
x1, Symbol -> Expr
F.EVar Symbol
x2)))
                              (forall c tv r.
Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
x2 RFInfo
i2 SpecType
t2 SpecType
t2'  RReft
r2)
        let t1x2' :: SpecType
t1x2' = SpecType
t1' forall a. Subable a => a -> (Symbol, Expr) -> a
`F.subst1` (Symbol
x1, Symbol -> Expr
F.EVar Symbol
x2)
        [FixSubC]
cs''     <- Bool -> SubC -> CG [FixSubC]
splitC Bool
allowTC  (CGEnv -> SpecType -> SpecType -> SubC
SubC CGEnv
γ' SpecType
t1x2' SpecType
t2')
        forall (m :: * -> *) a. Monad m => a -> m a
return    forall a b. (a -> b) -> a -> b
$ [FixSubC]
cs forall a. [a] -> [a] -> [a]
++ [FixSubC]
cs' forall a. [a] -> [a] -> [a]
++ [FixSubC]
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 [FixSubC]
cs    <- CGEnv -> SpecType -> SpecType -> CG [FixSubC]
bsplitC CGEnv
γ SpecType
t1 SpecType
t2
        [FixSubC]
cs'   <- Bool -> SubC -> CG [FixSubC]
splitC Bool
allowTC  (CGEnv -> SpecType -> SpecType -> SubC
SubC CGEnv
γ SpecType
r1 SpecType
r2)
        [FixSubC]
cs''  <- Bool -> SubC -> CG [FixSubC]
splitC Bool
allowTC  (CGEnv -> SpecType -> SpecType -> SubC
SubC CGEnv
γ SpecType
r1' SpecType
r2')
        [FixSubC]
cs''' <- Bool -> SubC -> CG [FixSubC]
splitC Bool
allowTC  (CGEnv -> SpecType -> SpecType -> SubC
SubC CGEnv
γ SpecType
r2' SpecType
r1')
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [FixSubC]
cs forall a. [a] -> [a] -> [a]
++ [FixSubC]
cs' forall a. [a] -> [a] -> [a]
++ [FixSubC]
cs'' forall a. [a] -> [a] -> [a]
++ [FixSubC]
cs'''

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

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

splitC Bool
allowTC (SubC CGEnv
γ t1' :: SpecType
t1'@(RAllT RTVU RTyCon RTyVar
α1 SpecType
t1 RReft
_) t2' :: SpecType
t2'@(RAllT RTVU RTyCon RTyVar
α2 SpecType
t2 RReft
_))
  |  RTVU RTyCon RTyVar
α1 forall a. Eq a => a -> a -> Bool
==  RTVU RTyCon RTyVar
α2
  = do CGEnv
γ'  <- forall b0.
CGEnv -> RTVar RTyVar (RType RTyCon RTyVar b0) -> CG CGEnv
updateEnv CGEnv
γ RTVU RTyCon RTyVar
α2
       [FixSubC]
cs  <- CGEnv -> SpecType -> SpecType -> CG [FixSubC]
bsplitC CGEnv
γ SpecType
t1' SpecType
t2'
       [FixSubC]
cs' <- Bool -> SubC -> CG [FixSubC]
splitC Bool
allowTC forall a b. (a -> b) -> a -> b
$ CGEnv -> SpecType -> SpecType -> SubC
SubC CGEnv
γ' SpecType
t1 (forall a. Subable a => Subst -> a -> a
F.subst Subst
su SpecType
t2)
       forall (m :: * -> *) a. Monad m => a -> m a
return ([FixSubC]
cs forall a. [a] -> [a] -> [a]
++ [FixSubC]
cs')
  | Bool
otherwise
  = do CGEnv
γ'  <- forall b0.
CGEnv -> RTVar RTyVar (RType RTyCon RTyVar b0) -> CG CGEnv
updateEnv CGEnv
γ RTVU RTyCon RTyVar
α2
       [FixSubC]
cs  <- CGEnv -> SpecType -> SpecType -> CG [FixSubC]
bsplitC CGEnv
γ SpecType
t1' SpecType
t2'
       [FixSubC]
cs' <- Bool -> SubC -> CG [FixSubC]
splitC Bool
allowTC forall a b. (a -> b) -> a -> b
$ CGEnv -> SpecType -> SpecType -> SubC
SubC CGEnv
γ' SpecType
t1 (forall a. Subable a => Subst -> a -> a
F.subst Subst
su SpecType
t2'')
       forall (m :: * -> *) a. Monad m => a -> m a
return ([FixSubC]
cs forall a. [a] -> [a] -> [a]
++ [FixSubC]
cs')
  where
    t2'' :: SpecType
t2'' = 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' (forall tv s. RTVar tv s -> tv
ty_var_value RTVU RTyCon RTyVar
α2, forall c tv r. tv -> r -> RType c tv r
RVar (forall tv s. RTVar tv s -> tv
ty_var_value RTVU RTyCon RTyVar
α1) forall a. Monoid a => a
mempty) SpecType
t2
    su :: Subst
su = case (forall s. RTVar RTyVar s -> Maybe (Symbol, s)
rTVarToBind RTVU RTyCon RTyVar
α1, forall s. RTVar RTyVar s -> Maybe (Symbol, s)
rTVarToBind RTVU RTyCon RTyVar
α2) of
          (Just (Symbol
x1, RType RTyCon RTyVar ()
_), Just (Symbol
x2, RType RTyCon RTyVar ()
_)) -> [(Symbol, Expr)] -> Subst
F.mkSubst [(Symbol
x1, Symbol -> Expr
F.EVar Symbol
x2)]
          (Maybe (Symbol, RType RTyCon RTyVar ()),
 Maybe (Symbol, RType RTyCon RTyVar ()))
_                            -> [(Symbol, Expr)] -> 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 forall c. TyConable c => c -> Bool
isEmbeddedDict else forall c. TyConable c => c -> Bool
isClass) RTyCon
c1 Bool -> Bool -> Bool
&& RTyCon
c1 forall a. Eq a => a -> a -> Bool
== RTyCon
c2
  = forall (m :: * -> *) a. Monad m => a -> m a
return []

splitC Bool
_ (SubC CGEnv
γ t1 :: SpecType
t1@RApp{} t2 :: SpecType
t2@RApp{})
  = do (SpecType
t1',SpecType
t2') <- SpecType -> SpecType -> CG (SpecType, SpecType)
unifyVV SpecType
t1 SpecType
t2
       [FixSubC]
cs    <- CGEnv -> SpecType -> SpecType -> CG [FixSubC]
bsplitC CGEnv
γ SpecType
t1' SpecType
t2'
       CGEnv
γ'    <- if Config -> Bool
bscope (forall t. HasConfig t => t -> Config
getConfig CGEnv
γ) then CGEnv
γ CGEnv -> SpecType -> CG CGEnv
`extendEnvWithVV` SpecType
t1' else forall (m :: * -> *) a. Monad m => a -> m a
return CGEnv
γ
       let RApp RTyCon
c [SpecType]
t1s [RTProp RTyCon RTyVar RReft]
r1s RReft
_ = SpecType
t1'
       let RApp RTyCon
_ [SpecType]
t2s [RTProp RTyCon RTyVar RReft]
r2s RReft
_ = SpecType
t2'
       let isapplied :: Bool
isapplied = Bool
True -- TC.tyConArity (rtc_tc c) == length t1s
       let tyInfo :: TyConInfo
tyInfo = RTyCon -> TyConInfo
rtc_info RTyCon
c
       [FixSubC]
csvar  <-  CGEnv -> [SpecType] -> [SpecType] -> [Variance] -> CG [FixSubC]
splitsCWithVariance           CGEnv
γ' [SpecType]
t1s [SpecType]
t2s forall a b. (a -> b) -> a -> b
$ TyConInfo -> [Variance]
varianceTyArgs TyConInfo
tyInfo
       [FixSubC]
csvar' <- Bool
-> CGEnv
-> [RTProp RTyCon RTyVar RReft]
-> [RTProp RTyCon RTyVar RReft]
-> [Variance]
-> CG [FixSubC]
rsplitsCWithVariance Bool
isapplied CGEnv
γ' [RTProp RTyCon RTyVar RReft]
r1s [RTProp RTyCon RTyVar RReft]
r2s forall a b. (a -> b) -> a -> b
$ TyConInfo -> [Variance]
variancePsArgs TyConInfo
tyInfo
       forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [FixSubC]
cs forall a. [a] -> [a] -> [a]
++ [FixSubC]
csvar forall a. [a] -> [a] -> [a]
++ [FixSubC]
csvar'

splitC Bool
_ (SubC CGEnv
γ t1 :: SpecType
t1@(RVar RTyVar
a1 RReft
_) t2 :: SpecType
t2@(RVar RTyVar
a2 RReft
_))
  | RTyVar
a1 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)
  = forall a. Maybe SrcSpan -> [Char] -> a
panic (forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ CGEnv -> SrcSpan
getLocation CGEnv
γ) forall a b. (a -> b) -> a -> b
$ [Char]
"(Another Broken Test!!!) splitc unexpected:\n" forall a. [a] -> [a] -> [a]
++ SpecType -> [Char]
traceTy SpecType
t1 forall a. [a] -> [a] -> [a]
++ [Char]
"\n  <:\n" forall a. [a] -> [a] -> [a]
++ SpecType -> [Char]
traceTy SpecType
t2

splitC Bool
_ (SubR CGEnv
γ Oblig
o RReft
r)
  = do Templates
ts     <- CG Templates
getTemplates
       let r1' :: SortedReft
r1' = SEnv Sort -> Templates -> SortedReft -> SortedReft
pruneUnsortedReft SEnv Sort
γ'' Templates
ts SortedReft
r1
       forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a.
IBindEnv
-> SortedReft
-> SortedReft
-> Maybe Integer
-> Tag
-> a
-> [SubC a]
F.subC IBindEnv
γ' SortedReft
r1' SortedReft
r2 forall a. Maybe a
Nothing Tag
tag Cinfo
ci
  where
    γ'' :: SEnv Sort
γ'' = FEnv -> SEnv Sort
feEnv forall a b. (a -> b) -> a -> b
$ CGEnv -> FEnv
fenv CGEnv
γ
    γ' :: IBindEnv
γ'  = FEnv -> IBindEnv
feBinds 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 forall a b. (a -> b) -> a -> b
$ (Symbol, Expr) -> Reft
F.Reft (Symbol
vv, Symbol -> Expr
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 = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall t.
SrcSpan -> Oblig -> Doc -> HashMap Symbol t -> t -> TError t
ErrAssType SrcSpan
src Oblig
o ([Char] -> Doc
text forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> [Char]
show Oblig
o forall a. [a] -> [a] -> [a]
++ [Char]
"type error") HashMap Symbol SpecType
g (Reft -> SpecType
rHole Reft
rr)
    rr :: Reft
rr  = forall r. Reftable r => r -> Reft
F.toReft RReft
r
    tag :: Tag
tag = CGEnv -> Tag
getTag CGEnv
γ
    src :: SrcSpan
src = CGEnv -> SrcSpan
getLocation CGEnv
γ
    g :: HashMap Symbol SpecType
g   = forall t. AREnv t -> HashMap Symbol t
reLocal forall a b. (a -> b) -> a -> b
$ CGEnv -> REnv
renv CGEnv
γ

traceTy :: SpecType -> String
traceTy :: SpecType -> [Char]
traceTy (RVar RTyVar
v RReft
_)      = [Char] -> [Char]
parens ([Char]
"RVar " forall a. [a] -> [a] -> [a]
++ 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 " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
showpp RTyCon
c forall a. [a] -> [a] -> [a]
++ [[Char]] -> [Char]
unwords (SpecType -> [Char]
traceTy forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SpecType]
ts))
traceTy (RAllP PVU RTyCon RTyVar
_ SpecType
t)     = [Char] -> [Char]
parens ([Char]
"RAllP " forall a. [a] -> [a] -> [a]
++ SpecType -> [Char]
traceTy SpecType
t)
traceTy (RAllT RTVU RTyCon RTyVar
_ SpecType
t RReft
_)   = [Char] -> [Char]
parens ([Char]
"RAllT " forall a. [a] -> [a] -> [a]
++ SpecType -> [Char]
traceTy SpecType
t)
traceTy (RFun Symbol
_ RFInfo
_ SpecType
t SpecType
t' RReft
_) = [Char] -> [Char]
parens ([Char]
"RFun " forall a. [a] -> [a] -> [a]
++ [Char] -> [Char]
parens (SpecType -> [Char]
traceTy SpecType
t) 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 " forall a. [a] -> [a] -> [a]
++ [Char] -> [Char]
parens (SpecType -> [Char]
traceTy SpecType
tx) 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 " forall a. [a] -> [a] -> [a]
++ [Char] -> [Char]
parens (SpecType -> [Char]
traceTy SpecType
tx) forall a. [a] -> [a] -> [a]
++ [Char] -> [Char]
parens (SpecType -> [Char]
traceTy SpecType
t))
traceTy (RExprArg Located Expr
_)    = [Char]
"RExprArg"
traceTy (RAppTy SpecType
t SpecType
t' RReft
_) = [Char] -> [Char]
parens ([Char]
"RAppTy " forall a. [a] -> [a] -> [a]
++ [Char] -> [Char]
parens (SpecType -> [Char]
traceTy SpecType
t) 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 " forall a. [a] -> [a] -> [a]
++ SpecType -> [Char]
traceTy SpecType
t)

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

rHole :: F.Reft -> SpecType
rHole :: Reft -> SpecType
rHole = forall c tv r. r -> RType c tv r
RHole forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall r. r -> UReft r
uTop


splitsCWithVariance :: CGEnv
                    -> [SpecType]
                    -> [SpecType]
                    -> [Variance]
                    -> CG [FixSubC]
splitsCWithVariance :: CGEnv -> [SpecType] -> [SpecType] -> [Variance] -> CG [FixSubC]
splitsCWithVariance CGEnv
γ [SpecType]
t1s [SpecType]
t2s [Variance]
variants
  = forall (m :: * -> *) (t :: * -> *) a b.
(Monad m, Traversable t) =>
(a -> m [b]) -> t a -> m [b]
concatMapM (\(SpecType
t1, SpecType
t2, Variance
v) -> 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 (forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)) (CGEnv -> SpecType -> SpecType -> SubC
SubC CGEnv
γ SpecType
s1 SpecType
s2)) SpecType
t1 SpecType
t2 Variance
v) (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]
_
  = forall (m :: * -> *) a. Monad m => a -> m a
return []

rsplitsCWithVariance Bool
_ CGEnv
γ [RTProp RTyCon RTyVar RReft]
t1s [RTProp RTyCon RTyVar RReft]
t2s [Variance]
variants
  = 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) -> 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) (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
  Templates
temp   <- CG Templates
getTemplates
  Bool
isHO   <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CGInfo -> Bool
allowHO
  SpecType
t1'    <- CGEnv -> SpecType -> SpecType
addLhsInv CGEnv
γ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). FreshM m => SpecType -> m SpecType
refreshVV SpecType
t1
  forall (m :: * -> *) a. Monad m => a -> m a
return  forall a b. (a -> b) -> a -> b
$ CGEnv -> SpecType -> SpecType -> Templates -> Bool -> [FixSubC]
bsplitC' CGEnv
γ SpecType
t1' SpecType
t2 Templates
temp Bool
isHO

addLhsInv :: CGEnv -> SpecType -> SpecType
addLhsInv :: CGEnv -> SpecType -> SpecType
addLhsInv CGEnv
γ SpecType
t = RTyConInv -> SpecType -> SpecType
addRTyConInv (CGEnv -> RTyConInv
invs CGEnv
γ) SpecType
t forall r c tv. Reftable r => RType c tv r -> r -> RType c tv r
`strengthen` RReft
r
  where
    r :: RReft
r         = (forall a. Monoid a => a
mempty :: UReft F.Reft) { ur_reft :: Reft
ur_reft = (Symbol, Expr) -> Reft
F.Reft (Symbol
F.dummySymbol, Expr
p) }
    p :: Expr
p         = REnv -> LConstraint -> Expr
constraintToLogic REnv
rE' (CGEnv -> LConstraint
lcs CGEnv
γ)
    rE' :: REnv
rE'       = Symbol -> SpecType -> REnv -> REnv
insertREnv Symbol
v SpecType
t (CGEnv -> REnv
renv CGEnv
γ)
    v :: Symbol
v         = 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
 = 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
&& forall r. Reftable r => r -> Bool
F.isNonTrivial SortedReft
r2'
 = forall a.
IBindEnv
-> SortedReft -> SortedReft -> Tag -> (SortedReft -> a) -> [SubC a]
mkSubC IBindEnv
γ' (SortedReft
r1' {sr_reft :: Reft
F.sr_reft = forall a. Monoid a => a
mempty}) SortedReft
r2' Tag
tag SortedReft -> Cinfo
ci
 | forall r. Reftable r => r -> Bool
F.isNonTrivial SortedReft
r2'
 = 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 forall a b. (a -> b) -> a -> b
$ CGEnv -> FEnv
fenv CGEnv
γ
    r1' :: SortedReft
r1' = 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' = 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   = forall t. AREnv t -> HashMap Symbol t
reLocal forall a b. (a -> b) -> a -> b
$ CGEnv -> REnv
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 = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a -> a
fromMaybe (forall t.
SrcSpan
-> Doc -> Maybe Integer -> HashMap Symbol t -> t -> t -> TError t
ErrSubType SrcSpan
src ([Char] -> Doc
text [Char]
"subtype") 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 = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\SortedReft
sr2' -> forall a.
IBindEnv
-> SortedReft
-> SortedReft
-> Maybe Integer
-> Tag
-> a
-> [SubC a]
F.subC IBindEnv
g SortedReft
sr1 SortedReft
sr2' 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, Expr
r))) = [ Sort -> Reft -> SortedReft
F.RR Sort
t ((Symbol, Expr) -> Reft
F.Reft (Symbol
v, Expr
ra)) | Expr
ra <- Expr -> [Expr]
refaConjuncts Expr
r ]

refaConjuncts :: F.Expr -> [F.Expr]
refaConjuncts :: Expr -> [Expr]
refaConjuncts Expr
p = [Expr
p' | Expr
p' <- Expr -> [Expr]
F.conjuncts Expr
p, Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ Expr -> Bool
F.isTautoPred Expr
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'  = forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp RTyCon
c [SpecType]
ts [RTProp RTyCon RTyVar RReft]
rs forall a b. (a -> b) -> a -> b
$ RReft -> SortedReft -> RReft
replaceReft RReft
r SortedReft
r'
replaceTop (RVar RTyVar
a RReft
r) SortedReft
r'        = forall c tv r. tv -> r -> RType c tv r
RVar RTyVar
a       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' = forall c tv r.
Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
b RFInfo
i SpecType
t1 SpecType
t2 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'  = forall c tv r. RType c tv r -> RType c tv r -> r -> RType c tv r
RAppTy SpecType
t1 SpecType
t2 forall a b. (a -> b) -> a -> b
$ RReft -> SortedReft -> RReft
replaceReft RReft
r SortedReft
r'
replaceTop (RAllT RTVU RTyCon RTyVar
a SpecType
t RReft
r)    SortedReft
r'  = forall c tv r. RTVU c tv -> RType c tv r -> r -> RType c tv r
RAllT RTVU RTyCon RTyVar
a SpecType
t    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 :: Reft
ur_reft = (Symbol, Expr) -> Reft
F.Reft (Symbol
v, forall a. Subable a => a -> (Symbol, Expr) -> a
F.subst1  Expr
p (Symbol
vr, Symbol -> Expr
F.EVar Symbol
v) )}
  where
    F.Reft (Symbol
v, Expr
_)         = forall r. UReft r -> r
ur_reft RReft
rr
    F.Reft (Symbol
vr,Expr
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 Symbol
vv <- Maybe Integer -> Symbol
F.vv forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. Freshable m a => m a
fresh
       forall (m :: * -> *) a. Monad m => a -> m a
return (forall c (f :: * -> *) tv.
(TyConable c, Reftable (f Reft), Functor f) =>
RType c tv (f Reft) -> Symbol -> RType c tv (f Reft)
shiftVV SpecType
t1 Symbol
vv, forall c (f :: * -> *) tv.
(TyConable c, Reftable (f Reft), Functor f) =>
RType c tv (f Reft) -> Symbol -> RType c tv (f Reft)
shiftVV SpecType
t2 Symbol
vv)

unifyVV SpecType
_ SpecType
_
  = forall a. Maybe SrcSpan -> [Char] -> a
panic 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
_))
  = forall a. Maybe SrcSpan -> [Char] -> a
panic forall a. Maybe a
Nothing [Char]
"RefTypes.rsplitC on RProp _ (RHole _)"

rsplitC CGEnv
_ (RProp [(Symbol, RType RTyCon RTyVar ())]
_ (RHole RReft
_)) RTProp RTyCon RTyVar RReft
_
  = forall a. Maybe SrcSpan -> [Char] -> a
panic 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
γ'  <-  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, 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]
       Bool -> SubC -> CG [FixSubC]
splitC (Config -> Bool
typeclass (forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)) (CGEnv -> SpecType -> SpecType -> SubC
SubC CGEnv
γ' (forall a. Subable a => Subst -> a -> a
F.subst Subst
su SpecType
r1) SpecType
r2)
  where su :: Subst
su = [(Symbol, Expr)] -> Subst
F.mkSubst [(Symbol
x, Symbol -> Expr
F.EVar Symbol
y) | ((Symbol
x,RType RTyCon RTyVar ()
_), (Symbol
y,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 forall r c tv. Reftable r => RType c tv r -> r -> RType c tv r
`strengthen` forall r. r -> UReft r
uTop Reft
r'
  where
    r' :: Reft
r'                = forall a. a -> Maybe a -> a
fromMaybe forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$ CGEnv -> Reft -> Maybe Reft
forallExprReft CGEnv
γ Reft
r
    r :: Reft
r                 = SortedReft -> Reft
F.sr_reft forall a b. (a -> b) -> a -> b
$ 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 Expr
e <- Reft -> Maybe Expr
F.isSingletonReft Reft
r
     CGEnv -> (Expr, [Expr]) -> Maybe Reft
forallExprReft_ CGEnv
γ forall a b. (a -> b) -> a -> b
$ Expr -> (Expr, [Expr])
F.splitEApp Expr
e

forallExprReft_ :: CGEnv -> (F.Expr, [F.Expr]) -> Maybe F.Reft
forallExprReft_ :: CGEnv -> (Expr, [Expr]) -> 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)  -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ SortedReft -> Reft
F.sr_reft forall a b. (a -> b) -> a -> b
$ 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         -> forall a. Maybe a
Nothing

forallExprReft_ CGEnv
γ (F.EVar Symbol
f, [Expr]
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, Expr)] -> Subst
F.mkSubst forall a b. (a -> b) -> a -> b
$ forall a b.
(?callStack::CallStack) =>
[Char] -> [a] -> [b] -> [(a, b)]
safeZip [Char]
"fExprRefType" [Symbol]
xs [Expr]
es in
                       forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. Subable a => Subst -> a -> a
F.subst Subst
su forall a b. (a -> b) -> a -> b
$ SortedReft -> Reft
F.sr_reft forall a b. (a -> b) -> a -> b
$ 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       -> forall a. Maybe a
Nothing

forallExprReft_ CGEnv
_ (Expr, [Expr])
_
  = 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 = Var -> ([Symbol], [RFInfo], [SpecType], [RReft], SpecType)
snap forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Symbol -> SEnv a -> Maybe a
F.lookupSEnv Symbol
sym (CGEnv -> SEnv Var
syenv CGEnv
γ)
  where
    snap :: Var -> ([Symbol], [RFInfo], [SpecType], [RReft], SpecType)
snap     = forall t t4 t0 t1 t2 t3.
(t -> t4) -> (t0, t1, t2, t3, t) -> (t0, t1, t2, t3, t4)
mapFifth5 forall t t1 t2. RType t t1 t2 -> RType t t1 t2
ignoreOblig forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\(([Symbol]
x,[RFInfo]
a,[SpecType]
b,[RReft]
c),SpecType
t)->([Symbol]
x,[RFInfo]
a,[SpecType]
b,[RReft]
c,SpecType
t)) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t t1 a.
RType t t1 a
-> (([Symbol], [RFInfo], [RType t t1 a], [a]), RType t t1 a)
bkArrow forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. (a, b, c) -> c
thd3 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall tv c r.
RType tv c r
-> ([(RTVar c (RType tv c ()), r)], [PVar (RType tv c ())],
    RType tv c r)
bkUniv forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {a}. (PPrint a, Symbolic a) => a -> SpecType
lookup'
    lookup' :: a -> SpecType
lookup' a
z = forall a. a -> Maybe a -> a
fromMaybe (forall x a. PPrint x => CGEnv -> x -> a
panicUnbound CGEnv
γ a
z) (CGEnv
γ (?callStack::CallStack) => CGEnv -> Symbol -> Maybe SpecType
?= forall a. Symbolic a => a -> Symbol
F.symbol a
z)


--------------------------------------------------------------------------------
getTag :: CGEnv -> F.Tag
--------------------------------------------------------------------------------
getTag :: CGEnv -> Tag
getTag CGEnv
γ = 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 = forall a e. Exception e => e -> a
Ex.throw (forall t. SrcSpan -> Doc -> TError t
ErrUnbound (CGEnv -> SrcSpan
getLocation CGEnv
γ) (forall a. PPrint a => a -> Doc
F.pprint x
x) :: Error)