{-# 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)
        [FixWfC] -> CG [FixWfC]
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ([FixWfC] -> CG [FixWfC]) -> [FixWfC] -> CG [FixWfC]
forall a b. (a -> b) -> a -> b
$ [FixWfC]
ws [FixWfC] -> [FixWfC] -> [FixWfC]
forall a. [a] -> [a] -> [a]
++ [FixWfC]
ws' [FixWfC] -> [FixWfC] -> [FixWfC]
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)
        [FixWfC] -> CG [FixWfC]
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ([FixWfC] -> CG [FixWfC]) -> [FixWfC] -> CG [FixWfC]
forall a b. (a -> b) -> a -> b
$ [FixWfC]
ws [FixWfC] -> [FixWfC] -> [FixWfC]
forall a. [a] -> [a] -> [a]
++ [FixWfC]
ws' [FixWfC] -> [FixWfC] -> [FixWfC]
forall a. [a] -> [a] -> [a]
++ [FixWfC]
ws''

splitW (WfC CGEnv
γ t' :: SpecType
t'@(RAllT RTVU RTyCon RTyVar
a SpecType
t RReft
_))
  = do CGEnv
γ'  <- CGEnv -> RTVU RTyCon RTyVar -> CG 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)
       [FixWfC] -> CG [FixWfC]
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ([FixWfC] -> CG [FixWfC]) -> [FixWfC] -> CG [FixWfC]
forall a b. (a -> b) -> a -> b
$ [FixWfC]
ws [FixWfC] -> [FixWfC] -> [FixWfC]
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 (CGEnv -> Config
forall t. HasConfig t => t -> Config
getConfig CGEnv
γ) then CGEnv
γ CGEnv -> SpecType -> CG CGEnv
`extendEnvWithVV` SpecType
t else CGEnv -> CG CGEnv
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return CGEnv
γ
        [FixWfC]
ws'   <- [[FixWfC]] -> [FixWfC]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[FixWfC]] -> [FixWfC])
-> StateT CGInfo Identity [[FixWfC]] -> CG [FixWfC]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (SpecType -> CG [FixWfC])
-> [SpecType] -> StateT CGInfo Identity [[FixWfC]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (WfC -> CG [FixWfC]
splitW (WfC -> CG [FixWfC])
-> (SpecType -> WfC) -> SpecType -> CG [FixWfC]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CGEnv -> SpecType -> WfC
WfC CGEnv
γ') [SpecType]
ts
        [FixWfC]
ws''  <- [[FixWfC]] -> [FixWfC]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[FixWfC]] -> [FixWfC])
-> StateT CGInfo Identity [[FixWfC]] -> CG [FixWfC]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (RTProp RTyCon RTyVar RReft -> CG [FixWfC])
-> [RTProp RTyCon RTyVar RReft]
-> StateT CGInfo Identity [[FixWfC]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (CGEnv -> RTProp RTyCon RTyVar RReft -> CG [FixWfC]
rsplitW CGEnv
γ)       [RTProp RTyCon RTyVar RReft]
rs
        [FixWfC] -> CG [FixWfC]
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ([FixWfC] -> CG [FixWfC]) -> [FixWfC] -> CG [FixWfC]
forall a b. (a -> b) -> a -> b
$ [FixWfC]
ws [FixWfC] -> [FixWfC] -> [FixWfC]
forall a. [a] -> [a] -> [a]
++ [FixWfC]
ws' [FixWfC] -> [FixWfC] -> [FixWfC]
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)
        [FixWfC] -> CG [FixWfC]
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ([FixWfC] -> CG [FixWfC]) -> [FixWfC] -> CG [FixWfC]
forall a b. (a -> b) -> a -> b
$ [FixWfC]
ws [FixWfC] -> [FixWfC] -> [FixWfC]
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)
        [FixWfC] -> CG [FixWfC]
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ([FixWfC] -> CG [FixWfC]) -> [FixWfC] -> CG [FixWfC]
forall a b. (a -> b) -> a -> b
$ [FixWfC]
ws [FixWfC] -> [FixWfC] -> [FixWfC]
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)
  = Maybe SrcSpan -> [Char] -> CG [FixWfC]
forall a. 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. 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
γ' <- (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]
  WfC -> CG [FixWfC]
splitW (WfC -> CG [FixWfC]) -> WfC -> CG [FixWfC]
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  <- (CGInfo -> Bool) -> StateT CGInfo Identity Bool
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CGInfo -> Bool
allowHO
     [FixWfC] -> CG [FixWfC]
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ([FixWfC] -> CG [FixWfC]) -> [FixWfC] -> CG [FixWfC]
forall a b. (a -> b) -> a -> b
$ CGEnv -> SpecType -> Templates -> Bool -> [FixWfC]
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
|| SortedReft -> Bool
forall r. Reftable r => r -> 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) -> RType RTyCon RTyVar a -> RType 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
γ 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 <- StateT CGInfo Identity Symbol
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 (SpecType -> (Symbol, Expr) -> SpecType
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 <- StateT CGInfo Identity Symbol
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
γ' (SpecType -> (Symbol, Expr) -> SpecType
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 Symbol -> Symbol -> Bool
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  <- StateT CGInfo Identity Symbol
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 SpecType -> (Symbol, Expr) -> SpecType
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  <- StateT CGInfo Identity Symbol
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 (SpecType -> (Symbol, Expr) -> SpecType
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
γ' <- (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
       [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 )
       [FixSubC] -> CG [FixSubC]
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ([FixSubC] -> CG [FixSubC]) -> [FixSubC] -> CG [FixSubC]
forall a b. (a -> b) -> a -> b
$ [FixSubC]
c1 [FixSubC] -> [FixSubC] -> [FixSubC]
forall a. [a] -> [a] -> [a]
++ [FixSubC]
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
γ' <- (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
       [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)
       [FixSubC] -> CG [FixSubC]
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ([FixSubC] -> CG [FixSubC]) -> [FixSubC] -> CG [FixSubC]
forall a b. (a -> b) -> a -> b
$ [FixSubC]
c1 [FixSubC] -> [FixSubC] -> [FixSubC]
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
γ (Symbol -> RFInfo -> SpecType -> SpecType -> RReft -> SpecType
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 RReft -> (Symbol, Expr) -> RReft
forall a. Subable a => a -> (Symbol, Expr) -> a
`F.subst1` (Symbol
x1, Symbol -> Expr
F.EVar Symbol
x2)))
                              (Symbol -> RFInfo -> SpecType -> SpecType -> RReft -> SpecType
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' SpecType -> (Symbol, Expr) -> SpecType
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')
        [FixSubC] -> CG [FixSubC]
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return    ([FixSubC] -> CG [FixSubC]) -> [FixSubC] -> CG [FixSubC]
forall a b. (a -> b) -> a -> b
$ [FixSubC]
cs [FixSubC] -> [FixSubC] -> [FixSubC]
forall a. [a] -> [a] -> [a]
++ [FixSubC]
cs' [FixSubC] -> [FixSubC] -> [FixSubC]
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')
        [FixSubC] -> CG [FixSubC]
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ([FixSubC] -> CG [FixSubC]) -> [FixSubC] -> CG [FixSubC]
forall a b. (a -> b) -> a -> b
$ [FixSubC]
cs [FixSubC] -> [FixSubC] -> [FixSubC]
forall a. [a] -> [a] -> [a]
++ [FixSubC]
cs' [FixSubC] -> [FixSubC] -> [FixSubC]
forall a. [a] -> [a] -> [a]
++ [FixSubC]
cs'' [FixSubC] -> [FixSubC] -> [FixSubC]
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 (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) -> RType RTyCon RTyVar a -> RType RTyCon RTyVar b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((UsedPVar, (Symbol, [((), Symbol, Expr)]) -> Expr)
-> RReft -> RReft
replacePredsWithRefs (UsedPVar, (Symbol, [((), Symbol, Expr)]) -> Expr)
forall {a} {b}. (UsedPVar, (Symbol, [(a, b, Expr)]) -> Expr)
su) SpecType
t
    su :: (UsedPVar, (Symbol, [(a, b, Expr)]) -> Expr)
su = (PVU RTyCon RTyVar -> UsedPVar
forall t. PVar t -> UsedPVar
uPVar PVU RTyCon RTyVar
p, PVU RTyCon RTyVar -> (Symbol, [(a, b, Expr)]) -> Expr
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)
  = Maybe SrcSpan -> [Char] -> CG [FixSubC]
forall a. 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 RTVU RTyCon RTyVar
α1 SpecType
t1 RReft
_) t2' :: SpecType
t2'@(RAllT RTVU RTyCon RTyVar
α2 SpecType
t2 RReft
_))
  |  RTVU RTyCon RTyVar
α1 RTVU RTyCon RTyVar -> RTVU RTyCon RTyVar -> Bool
forall a. Eq a => a -> a -> Bool
==  RTVU RTyCon RTyVar
α2
  = do CGEnv
γ'  <- CGEnv -> RTVU RTyCon RTyVar -> CG 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 (SubC -> CG [FixSubC]) -> SubC -> CG [FixSubC]
forall a b. (a -> b) -> a -> b
$ CGEnv -> SpecType -> SpecType -> SubC
SubC CGEnv
γ' SpecType
t1 (Subst -> SpecType -> SpecType
forall a. Subable a => Subst -> a -> a
F.subst Subst
su SpecType
t2)
       [FixSubC] -> CG [FixSubC]
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ([FixSubC]
cs [FixSubC] -> [FixSubC] -> [FixSubC]
forall a. [a] -> [a] -> [a]
++ [FixSubC]
cs')
  | Bool
otherwise
  = do CGEnv
γ'  <- CGEnv -> RTVU RTyCon RTyVar -> CG 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 (SubC -> CG [FixSubC]) -> SubC -> CG [FixSubC]
forall a b. (a -> b) -> a -> b
$ CGEnv -> SpecType -> SpecType -> SubC
SubC CGEnv
γ' SpecType
t1 (Subst -> SpecType -> SpecType
forall a. Subable a => Subst -> a -> a
F.subst Subst
su SpecType
t2'')
       [FixSubC] -> CG [FixSubC]
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ([FixSubC]
cs [FixSubC] -> [FixSubC] -> [FixSubC]
forall a. [a] -> [a] -> [a]
++ [FixSubC]
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' (RTVU RTyCon RTyVar -> RTyVar
forall tv s. RTVar tv s -> tv
ty_var_value RTVU RTyCon RTyVar
α2, RTyVar -> RReft -> SpecType
forall c tv r. tv -> r -> RType c tv r
RVar (RTVU RTyCon RTyVar -> RTyVar
forall tv s. RTVar tv s -> tv
ty_var_value RTVU RTyCon RTyVar
α1) RReft
forall a. Monoid a => a
mempty) SpecType
t2
    su :: Subst
su = case (RTVU RTyCon RTyVar -> Maybe (Symbol, RType RTyCon RTyVar ())
forall s. RTVar RTyVar s -> Maybe (Symbol, s)
rTVarToBind RTVU RTyCon RTyVar
α1, RTVU RTyCon RTyVar -> Maybe (Symbol, RType RTyCon RTyVar ())
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 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 (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 (CGEnv -> Config
forall t. HasConfig t => t -> Config
getConfig CGEnv
γ) then CGEnv
γ CGEnv -> SpecType -> CG CGEnv
`extendEnvWithVV` SpecType
t1' else CGEnv -> CG CGEnv
forall a. a -> StateT CGInfo Identity a
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 ([Variance] -> CG [FixSubC]) -> [Variance] -> CG [FixSubC]
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 ([Variance] -> CG [FixSubC]) -> [Variance] -> CG [FixSubC]
forall a b. (a -> b) -> a -> b
$ TyConInfo -> [Variance]
variancePsArgs TyConInfo
tyInfo
       [FixSubC] -> CG [FixSubC]
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ([FixSubC] -> CG [FixSubC]) -> [FixSubC] -> CG [FixSubC]
forall a b. (a -> b) -> a -> b
$ [FixSubC]
cs [FixSubC] -> [FixSubC] -> [FixSubC]
forall a. [a] -> [a] -> [a]
++ [FixSubC]
csvar [FixSubC] -> [FixSubC] -> [FixSubC]
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 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. 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 Templates
ts     <- CG Templates
getTemplates
       let r1' :: SortedReft
r1' = SEnv Sort -> Templates -> SortedReft -> SortedReft
pruneUnsortedReft SEnv Sort
γ'' Templates
ts SortedReft
r1
       [FixSubC] -> CG [FixSubC]
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ([FixSubC] -> CG [FixSubC]) -> [FixSubC] -> CG [FixSubC]
forall a b. (a -> b) -> a -> b
$ IBindEnv
-> SortedReft
-> SortedReft
-> Maybe Integer
-> Tag
-> Cinfo
-> [FixSubC]
forall a.
IBindEnv
-> SortedReft
-> SortedReft
-> Maybe Integer
-> Tag
-> a
-> [SubC a]
F.subC IBindEnv
γ' SortedReft
r1' SortedReft
r2 Maybe Integer
forall a. Maybe a
Nothing Tag
tag Cinfo
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, 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 = 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
F.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 PVU RTyCon RTyVar
_ SpecType
t)     = [Char] -> [Char]
parens ([Char]
"RAllP " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SpecType -> [Char]
traceTy SpecType
t)
traceTy (RAllT RTVU 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 Expr
_)    = [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 c tv r. r -> RType c tv r
RHole (RReft -> SpecType) -> (Reft -> RReft) -> Reft -> SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Reft -> RReft
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
  = ((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
  Templates
temp   <- CG Templates
getTemplates
  Bool
isHO   <- (CGInfo -> Bool) -> StateT CGInfo Identity Bool
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CGInfo -> Bool
allowHO
  SpecType
t1'    <- CGEnv -> SpecType -> SpecType
addLhsInv CGEnv
γ (SpecType -> SpecType)
-> StateT CGInfo Identity SpecType
-> StateT CGInfo Identity SpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SpecType -> StateT CGInfo Identity SpecType
forall (m :: * -> *). FreshM m => SpecType -> m SpecType
refreshVV SpecType
t1
  [FixSubC] -> CG [FixSubC]
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return  ([FixSubC] -> CG [FixSubC]) -> [FixSubC] -> CG [FixSubC]
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 SpecType -> RReft -> SpecType
forall r c tv. Reftable r => RType c tv r -> r -> RType 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 :: Expr
p         = AREnv SpecType -> LConstraint -> Expr
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
forall r. Reftable r => r -> 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
forall r. Reftable r => r -> 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, 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 (Bool -> Bool) -> Bool -> Bool
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'  = RTyCon
-> [SpecType] -> [RTProp RTyCon RTyVar RReft] -> RReft -> SpecType
forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp RTyCon
c [SpecType]
ts [RTProp RTyCon RTyVar RReft]
rs (RReft -> 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 c tv r. tv -> r -> RType 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 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 (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 c tv r. RType c tv r -> RType c tv r -> r -> RType 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 RTVU RTyCon RTyVar
a SpecType
t RReft
r)    SortedReft
r'  = RTVU RTyCon RTyVar -> SpecType -> RReft -> SpecType
forall c tv r. RTVU c tv -> RType c tv r -> r -> RType c tv r
RAllT RTVU 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, Expr
_)         = RReft -> Reft
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 (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
       (SpecType, SpecType) -> CG (SpecType, SpecType)
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (SpecType -> Symbol -> SpecType
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, SpecType -> Symbol -> SpecType
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
_
  = Maybe SrcSpan -> [Char] -> CG (SpecType, SpecType)
forall a. 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. 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. 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
γ'  <-  (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]
       Bool -> SubC -> CG [FixSubC]
splitC (Config -> Bool
typeclass (CGEnv -> Config
forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)) (CGEnv -> SpecType -> SpecType -> SubC
SubC CGEnv
γ' (Subst -> SpecType -> SpecType
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 ()
_)) <- [(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 c tv. Reftable r => RType c tv r -> r -> RType c tv r
`strengthen` Reft -> RReft
forall r. r -> UReft 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 Expr
e <- Reft -> Maybe Expr
F.isSingletonReft Reft
r
     CGEnv -> (Expr, [Expr]) -> Maybe Reft
forallExprReft_ CGEnv
γ ((Expr, [Expr]) -> Maybe Reft) -> (Expr, [Expr]) -> Maybe Reft
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)  -> 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, [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 ([(Symbol, Expr)] -> Subst) -> [(Symbol, Expr)] -> Subst
forall a b. (a -> b) -> a -> b
$ [Char] -> [Symbol] -> [Expr] -> [(Symbol, Expr)]
forall a b.
(?callStack::CallStack) =>
[Char] -> [a] -> [b] -> [(a, b)]
safeZip [Char]
"fExprRefType" [Symbol]
xs [Expr]
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
_ (Expr, [Expr])
_
  = 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 = Var -> ([Symbol], [RFInfo], [SpecType], [RReft], SpecType)
snap (Var -> ([Symbol], [RFInfo], [SpecType], [RReft], SpecType))
-> Maybe Var
-> Maybe ([Symbol], [RFInfo], [SpecType], [RReft], SpecType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Symbol -> SEnv Var -> Maybe Var
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     = (SpecType -> SpecType)
-> ([Symbol], [RFInfo], [SpecType], [RReft], SpecType)
-> ([Symbol], [RFInfo], [SpecType], [RReft], SpecType)
forall t t4 t0 t1 t2 t3.
(t -> t4) -> (t0, t1, t2, t3, t) -> (t0, t1, t2, t3, t4)
mapFifth5 SpecType -> SpecType
forall t t1 t2. RType t t1 t2 -> RType t t1 t2
ignoreOblig (([Symbol], [RFInfo], [SpecType], [RReft], SpecType)
 -> ([Symbol], [RFInfo], [SpecType], [RReft], SpecType))
-> (Var -> ([Symbol], [RFInfo], [SpecType], [RReft], SpecType))
-> Var
-> ([Symbol], [RFInfo], [SpecType], [RReft], SpecType)
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)) ((([Symbol], [RFInfo], [SpecType], [RReft]), SpecType)
 -> ([Symbol], [RFInfo], [SpecType], [RReft], SpecType))
-> (Var -> (([Symbol], [RFInfo], [SpecType], [RReft]), SpecType))
-> Var
-> ([Symbol], [RFInfo], [SpecType], [RReft], SpecType)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SpecType -> (([Symbol], [RFInfo], [SpecType], [RReft]), SpecType)
forall t t1 a.
RType t t1 a
-> (([Symbol], [RFInfo], [RType t t1 a], [a]), RType t t1 a)
bkArrow (SpecType -> (([Symbol], [RFInfo], [SpecType], [RReft]), SpecType))
-> (Var -> SpecType)
-> Var
-> (([Symbol], [RFInfo], [SpecType], [RReft]), SpecType)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([(RTVU RTyCon RTyVar, RReft)], [PVU RTyCon RTyVar], SpecType)
-> SpecType
forall a b c. (a, b, c) -> c
thd3 (([(RTVU RTyCon RTyVar, RReft)], [PVU RTyCon RTyVar], SpecType)
 -> SpecType)
-> (Var
    -> ([(RTVU RTyCon RTyVar, RReft)], [PVU RTyCon RTyVar], SpecType))
-> Var
-> SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SpecType
-> ([(RTVU RTyCon RTyVar, RReft)], [PVU RTyCon RTyVar], SpecType)
forall tv c r.
RType tv c r
-> ([(RTVar c (RType tv c ()), r)], [PVar (RType tv c ())],
    RType tv c r)
bkUniv (SpecType
 -> ([(RTVU RTyCon RTyVar, RReft)], [PVU RTyCon RTyVar], SpecType))
-> (Var -> SpecType)
-> Var
-> ([(RTVU RTyCon RTyVar, RReft)], [PVU RTyCon RTyVar], SpecType)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> SpecType
forall {a}. (PPrint a, Symbolic a) => a -> SpecType
lookup'
    lookup' :: a -> SpecType
lookup' a
z = SpecType -> Maybe SpecType -> SpecType
forall a. a -> Maybe a -> a
fromMaybe (CGEnv -> a -> SpecType
forall x a. PPrint x => CGEnv -> x -> a
panicUnbound CGEnv
γ a
z) (CGEnv
γ (?callStack::CallStack) => 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. 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)