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

--------------------------------------------------------------------------------
-- | 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 (get)
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 SpecType
t1 SpecType
t2 RReft
_))
  =  do [FixWfC]
ws'  <- WfC -> CG [FixWfC]
splitW (CGEnv -> SpecType -> WfC
WfC CGEnv
γ SpecType
t1)
        CGEnv
γ'   <- CGEnv
γ CGEnv -> (String, Symbol, SpecType) -> CG CGEnv
+= (String
"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 (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@(RImpF Symbol
x SpecType
t1 SpecType
t2 RReft
_))
  =  do [FixWfC]
ws'  <- WfC -> CG [FixWfC]
splitW (CGEnv -> SpecType -> WfC
WfC CGEnv
γ SpecType
t1)
        CGEnv
γ'   <- CGEnv
γ CGEnv -> (String, Symbol, SpecType) -> CG CGEnv
+= (String
"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 (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 (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 (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 (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)
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)
mapM (CGEnv -> RTProp RTyCon RTyVar RReft -> CG [FixWfC]
rsplitW CGEnv
γ)       [RTProp RTyCon RTyVar RReft]
rs
        [FixWfC] -> CG [FixWfC]
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 -> (String, Symbol, SpecType) -> CG CGEnv
+= (String
"splitW1", Symbol
x, SpecType
tx)
        [FixWfC]
ws' <- WfC -> CG [FixWfC]
splitW (CGEnv -> SpecType -> WfC
WfC CGEnv
γ' SpecType
t)
        [FixWfC] -> CG [FixWfC]
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 -> (String, Symbol, SpecType) -> CG CGEnv
+= (String
"splitW2", Symbol
x, SpecType
tx)
        [FixWfC]
ws' <- WfC -> CG [FixWfC]
splitW (CGEnv -> SpecType -> WfC
WfC CGEnv
γ' SpecType
t)
        [FixWfC] -> CG [FixWfC]
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 -> String -> CG [FixWfC]
forall a. Maybe SrcSpan -> String -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing (String -> CG [FixWfC]) -> String -> CG [FixWfC]
forall a b. (a -> b) -> a -> b
$ String
"splitW cannot handle: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SpecType -> String
forall a. PPrint a => a -> String
showpp SpecType
t

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

rsplitW CGEnv
γ (RProp [(Symbol, RSort)]
ss SpecType
t0) = do
  CGEnv
γ' <- (CGEnv -> (String, Symbol, SpecType) -> CG CGEnv)
-> CGEnv -> [(String, Symbol, SpecType)] -> CG CGEnv
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM CGEnv -> (String, Symbol, SpecType) -> CG CGEnv
(+=) CGEnv
γ [(String
"rsplitW", Symbol
x, RSort -> SpecType
forall r c tv. Reftable r => RType c tv () -> RType c tv r
ofRSort RSort
s) | (Symbol
x, RSort
s) <- [(Symbol, RSort)]
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
allowHO   (CGInfo -> Bool)
-> StateT CGInfo Identity CGInfo -> StateT CGInfo Identity Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT CGInfo Identity CGInfo
forall s (m :: * -> *). MonadState s m => m s
get
     [FixWfC] -> CG [FixWfC]
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 RSort 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' :: 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 RSort 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 :: (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 (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 (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 :: 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 -> (String, Symbol, SpecType) -> CG CGEnv
+= (String
"splitS RAllT", Symbol
x, (b0 -> RReft) -> RType RTyCon RTyVar b0 -> SpecType
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 (m :: * -> *) a. Monad m => a -> m a
return CGEnv
γ

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

splitC :: SubC -> CG [FixSubC]
splitC (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 -> (String, Symbol, SpecType) -> CG CGEnv
+= (String
"addExBind 0", Symbol
x, CGEnv -> SpecType -> SpecType
forallExprRefType CGEnv
γ SpecType
tx)
       SubC -> CG [FixSubC]
splitC (CGEnv -> SpecType -> SpecType -> SubC
SubC CGEnv
γ' SpecType
t1 SpecType
t2)

splitC (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 -> (String, Symbol, SpecType) -> CG CGEnv
+= (String
"addExBind 1", Symbol
y, CGEnv -> SpecType -> SpecType
forallExprRefType CGEnv
γ SpecType
tx)
       SubC -> CG [FixSubC]
splitC (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 (SubC CGEnv
γ (REx Symbol
x SpecType
tx SpecType
t1) SpecType
t2)
  = do -- let tx' = traceShow ("splitC: " ++ showpp z) tx
       Symbol
y <- StateT CGInfo Identity Symbol
forall (m :: * -> *) a. Freshable m a => m a
fresh
       CGEnv
γ' <- CGEnv
γ CGEnv -> (String, Symbol, SpecType) -> CG CGEnv
+= (String
"addExBind 2", Symbol
y, CGEnv -> SpecType -> SpecType
forallExprRefType CGEnv
γ SpecType
tx)
       SubC -> CG [FixSubC]
splitC (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 (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 -> (String, Symbol, SpecType) -> CG CGEnv
+= (String
"addAllBind 3", Symbol
x, CGEnv -> SpecType -> SpecType
forallExprRefType CGEnv
γ SpecType
tx)
       SubC -> CG [FixSubC]
splitC (CGEnv -> SpecType -> SpecType -> SubC
SubC CGEnv
γ' SpecType
t1 SpecType
t2)

splitC (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 -> (String, Symbol, SpecType) -> CG CGEnv
+= (String
"addAABind 1", Symbol
y, CGEnv -> SpecType -> SpecType
forallExprRefType CGEnv
γ SpecType
tx)
       SubC -> CG [FixSubC]
splitC (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 (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 -> (String, Symbol, SpecType) -> CG CGEnv
+= (String
"addAllBind 2", Symbol
y, CGEnv -> SpecType -> SpecType
forallExprRefType CGEnv
γ SpecType
tx)
       SubC -> CG [FixSubC]
splitC (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 (SubC 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 -> (String, Symbol, SpecType) -> CG CGEnv
`addSEnv` (String
"splitS", Symbol
x,SpecType
t)) CGEnv
γ [(Symbol, SpecType)]
xts
       [FixSubC]
c1 <- SubC -> CG [FixSubC]
splitC (CGEnv -> SpecType -> SpecType -> SubC
SubC CGEnv
γ' SpecType
t1' SpecType
t2')
       [FixSubC]
c2 <- SubC -> CG [FixSubC]
splitC (CGEnv -> SpecType -> SpecType -> SubC
SubC CGEnv
γ  SpecType
t1  SpecType
t2 )
       [FixSubC] -> CG [FixSubC]
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 (SubC 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 -> (String, Symbol, SpecType) -> CG CGEnv
`addSEnv` (String
"splitS", Symbol
x,SpecType
t)) CGEnv
γ [(Symbol, SpecType)]
e
       [FixSubC]
c1 <- SubC -> CG [FixSubC]
splitC (CGEnv -> Oblig -> RReft -> SubC
SubR CGEnv
γ' Oblig
o  RReft
r)
       [FixSubC]
c2 <- SubC -> CG [FixSubC]
splitC (CGEnv -> SpecType -> SpecType -> SubC
SubC CGEnv
γ SpecType
t1 SpecType
t2)
       [FixSubC] -> CG [FixSubC]
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 (SubC CGEnv
γ (RFun Symbol
x1 SpecType
t1 SpecType
t1' RReft
r1) (RFun Symbol
x2 SpecType
t2 SpecType
t2' RReft
r2))
  =  do [FixSubC]
cs'      <- SubC -> CG [FixSubC]
splitC  (CGEnv -> SpecType -> SpecType -> SubC
SubC CGEnv
γ SpecType
t2 SpecType
t1)
        CGEnv
γ'       <- CGEnv
γCGEnv -> (String, Symbol, SpecType) -> CG CGEnv
+= (String
"splitC", Symbol
x2, SpecType
t2)
        [FixSubC]
cs       <- CGEnv -> SpecType -> SpecType -> CG [FixSubC]
bsplitC CGEnv
γ (Symbol -> SpecType -> SpecType -> RReft -> SpecType
forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
x1 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 -> SpecType -> SpecType -> RReft -> SpecType
forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
x2 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''     <- SubC -> CG [FixSubC]
splitC  (CGEnv -> SpecType -> SpecType -> SubC
SubC CGEnv
γ' SpecType
t1x2' SpecType
t2')
        [FixSubC] -> CG [FixSubC]
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 (SubC CGEnv
γ (RImpF Symbol
x1 SpecType
t1 SpecType
t1' RReft
r1) (RImpF Symbol
x2 SpecType
t2 SpecType
t2' RReft
r2))
  =  do [FixSubC]
cs'      <- SubC -> CG [FixSubC]
splitC  (CGEnv -> SpecType -> SpecType -> SubC
SubC CGEnv
γ SpecType
t2 SpecType
t1)
        CGEnv
γ'       <- CGEnv
γCGEnv -> (String, Symbol, SpecType) -> CG CGEnv
+= (String
"splitC", Symbol
x2, SpecType
t2)
        [FixSubC]
cs       <- CGEnv -> SpecType -> SpecType -> CG [FixSubC]
bsplitC CGEnv
γ (Symbol -> SpecType -> SpecType -> RReft -> SpecType
forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> r -> RType c tv r
RImpF Symbol
x1 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 -> SpecType -> SpecType -> RReft -> SpecType
forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> r -> RType c tv r
RImpF Symbol
x2 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''     <- SubC -> CG [FixSubC]
splitC  (CGEnv -> SpecType -> SpecType -> SubC
SubC CGEnv
γ' SpecType
t1x2' SpecType
t2')
        [FixSubC] -> CG [FixSubC]
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 (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'   <- SubC -> CG [FixSubC]
splitC  (CGEnv -> SpecType -> SpecType -> SubC
SubC CGEnv
γ SpecType
r1 SpecType
r2)
        [FixSubC]
cs''  <- SubC -> CG [FixSubC]
splitC  (CGEnv -> SpecType -> SpecType -> SubC
SubC CGEnv
γ SpecType
r1' SpecType
r2')
        [FixSubC]
cs''' <- SubC -> CG [FixSubC]
splitC  (CGEnv -> SpecType -> SpecType -> SubC
SubC CGEnv
γ SpecType
r2' SpecType
r1')
        [FixSubC] -> CG [FixSubC]
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 (SubC CGEnv
γ SpecType
t1 (RAllP PVU RTyCon RTyVar
p SpecType
t))
  = SubC -> CG [FixSubC]
splitC (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 (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 (SubC CGEnv
γ t1 :: SpecType
t1@(RAllP PVU RTyCon RTyVar
_ SpecType
_) SpecType
t2)
  = Maybe SrcSpan -> String -> CG [FixSubC]
forall a. Maybe SrcSpan -> String -> 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
γ) (String -> CG [FixSubC]) -> String -> CG [FixSubC]
forall a b. (a -> b) -> a -> b
$ String
"Predicate in lhs of constraint:" String -> String -> String
forall a. [a] -> [a] -> [a]
++ SpecType -> String
forall a. PPrint a => a -> String
showpp SpecType
t1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n<:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ SpecType -> String
forall a. PPrint a => a -> String
showpp SpecType
t2

splitC (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' <- SubC -> CG [FixSubC]
splitC (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 (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' <- SubC -> CG [FixSubC]
splitC (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 (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
subsTyVar_meet' (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, RSort)
forall s. RTVar RTyVar s -> Maybe (Symbol, s)
rTVarToBind RTVU RTyCon RTyVar
α1, RTVU RTyCon RTyVar -> Maybe (Symbol, RSort)
forall s. RTVar RTyVar s -> Maybe (Symbol, s)
rTVarToBind RTVU RTyCon RTyVar
α2) of
          (Just (Symbol
x1, RSort
_), Just (Symbol
x2, RSort
_)) -> [(Symbol, Expr)] -> Subst
F.mkSubst [(Symbol
x1, Symbol -> Expr
F.EVar Symbol
x2)]
          (Maybe (Symbol, RSort), Maybe (Symbol, RSort))
_                            -> [(Symbol, Expr)] -> Subst
F.mkSubst []

splitC (SubC CGEnv
_ (RApp RTyCon
c1 [SpecType]
_ [RTProp RTyCon RTyVar RReft]
_ RReft
_) (RApp RTyCon
c2 [SpecType]
_ [RTProp RTyCon RTyVar RReft]
_ RReft
_)) | 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 (m :: * -> *) a. Monad m => a -> m a
return []

splitC (SubC CGEnv
γ t1 :: SpecType
t1@(RApp RTyCon
_ [SpecType]
_ [RTProp RTyCon RTyVar RReft]
_ RReft
_) t2 :: SpecType
t2@(RApp RTyCon
_ [SpecType]
_ [RTProp RTyCon RTyVar RReft]
_ RReft
_))
  = 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 (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 (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 (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 (SubC CGEnv
γ SpecType
t1 SpecType
t2)
  = Maybe SrcSpan -> String -> CG [FixSubC]
forall a. Maybe SrcSpan -> String -> 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
γ) (String -> CG [FixSubC]) -> String -> CG [FixSubC]
forall a b. (a -> b) -> a -> b
$ String
"(Another Broken Test!!!) splitc unexpected:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ SpecType -> String
traceTy SpecType
t1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n  <:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ SpecType -> String
traceTy SpecType
t2

splitC (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 (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 (String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ Oblig -> String
forall a. Show a => a -> String
show Oblig
o String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"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 -> String
traceTy (RVar RTyVar
v RReft
_)      = String -> String
parens (String
"RVar " String -> String -> String
forall a. [a] -> [a] -> [a]
++ RTyVar -> String
forall a. PPrint a => a -> String
showpp RTyVar
v)
traceTy (RApp RTyCon
c [SpecType]
ts [RTProp RTyCon RTyVar RReft]
_ RReft
_) = String -> String
parens (String
"RApp " String -> String -> String
forall a. [a] -> [a] -> [a]
++ RTyCon -> String
forall a. PPrint a => a -> String
showpp RTyCon
c String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords (SpecType -> String
traceTy (SpecType -> String) -> [SpecType] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SpecType]
ts)) 
traceTy (RAllP PVU RTyCon RTyVar
_ SpecType
t)     = String -> String
parens (String
"RAllP " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SpecType -> String
traceTy SpecType
t)
traceTy (RAllT RTVU RTyCon RTyVar
_ SpecType
t RReft
_)   = String -> String
parens (String
"RAllT " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SpecType -> String
traceTy SpecType
t)
traceTy (RImpF Symbol
_ SpecType
t SpecType
t' RReft
_) = String -> String
parens (String
"RImpF " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
parens (SpecType -> String
traceTy SpecType
t) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
parens (SpecType -> String
traceTy SpecType
t'))
traceTy (RFun Symbol
_ SpecType
t SpecType
t' RReft
_) = String -> String
parens (String
"RFun " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
parens (SpecType -> String
traceTy SpecType
t) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
parens (SpecType -> String
traceTy SpecType
t'))
traceTy (RAllE Symbol
_ SpecType
tx SpecType
t)  = String -> String
parens (String
"RAllE " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
parens (SpecType -> String
traceTy SpecType
tx) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
parens (SpecType -> String
traceTy SpecType
t))
traceTy (REx Symbol
_ SpecType
tx SpecType
t)    = String -> String
parens (String
"REx " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
parens (SpecType -> String
traceTy SpecType
tx) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
parens (SpecType -> String
traceTy SpecType
t))
traceTy (RExprArg Located Expr
_)    = String
"RExprArg"
traceTy (RAppTy SpecType
t SpecType
t' RReft
_) = String -> String
parens (String
"RAppTy " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
parens (SpecType -> String
traceTy SpecType
t) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
parens (SpecType -> String
traceTy SpecType
t'))
traceTy (RHole RReft
_)       = String
"rHole"
traceTy (RRTy [(Symbol, SpecType)]
_ RReft
_ Oblig
_ SpecType
t)  = String -> String
parens (String
"RRTy " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SpecType -> String
traceTy SpecType
t)

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

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 -> (SubC -> CG [FixSubC]
splitC (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 (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
allowHO   (CGInfo -> Bool)
-> StateT CGInfo Identity CGInfo -> StateT CGInfo Identity Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT CGInfo Identity CGInfo
forall s (m :: * -> *). MonadState s m => m s
get
  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 (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 :: Reft
ur_reft = (Symbol, Expr) -> Reft
F.Reft (Symbol
F.dummySymbol, Expr
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
-> 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
 | SortedReft -> Bool
F.isFunctionSortedReft SortedReft
r1' Bool -> Bool -> Bool
&& SortedReft -> Bool
forall r. Reftable r => r -> Bool
F.isNonTrivial SortedReft
r2'
 = IBindEnv
-> SortedReft
-> SortedReft
-> Maybe Integer
-> Tag
-> Cinfo
-> [FixSubC]
forall a.
IBindEnv
-> SortedReft
-> SortedReft
-> Maybe Integer
-> Tag
-> a
-> [SubC a]
F.subC IBindEnv
γ' (SortedReft
r1' {sr_reft :: Reft
F.sr_reft = Reft
forall a. Monoid a => a
mempty}) SortedReft
r2' Maybe Integer
forall a. Maybe a
Nothing Tag
tag Cinfo
ci
 | SortedReft -> Bool
forall r. Reftable r => r -> Bool
F.isNonTrivial SortedReft
r2'
 = 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
 | 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 RSort 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 RSort r,
 Reftable (RTProp RTyCon RTyVar r)) =>
CGEnv -> Templates -> RRType r -> SortedReft
rTypeSortedReft' CGEnv
γ Templates
tem SpecType
t2
    ci :: Cinfo
ci  = SrcSpan -> Maybe Error -> Maybe Var -> Cinfo
Ci SrcSpan
src Maybe Error
err (CGEnv -> Maybe Var
cgVar CGEnv
γ)
    tag :: Tag
tag = CGEnv -> Tag
getTag CGEnv
γ
    -- err = Just $ ErrSubType src "subtype" g t1 t2
    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
$ Error -> Maybe Error -> Error
forall a. a -> Maybe a -> a
fromMaybe (SrcSpan
-> Doc -> HashMap Symbol SpecType -> SpecType -> SpecType -> Error
forall t. SrcSpan -> Doc -> HashMap Symbol t -> t -> t -> TError t
ErrSubType SrcSpan
src (String -> Doc
text String
"subtype") HashMap Symbol SpecType
g SpecType
t1 SpecType
t2) (CGEnv -> Maybe Error
cerr 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
γ

unifyVV :: SpecType -> SpecType -> CG (SpecType, SpecType)
unifyVV :: SpecType -> SpecType -> CG (SpecType, SpecType)
unifyVV t1 :: SpecType
t1@(RApp RTyCon
_ [SpecType]
_ [RTProp RTyCon RTyVar RReft]
_ RReft
_) t2 :: SpecType
t2@(RApp RTyCon
_ [SpecType]
_ [RTProp RTyCon RTyVar RReft]
_ RReft
_)
  = 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 (m :: * -> *) a. Monad m => a -> m a
return  ((SpecType, SpecType) -> CG (SpecType, SpecType))
-> (SpecType, SpecType) -> CG (SpecType, SpecType)
forall a b. (a -> b) -> a -> b
$ (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 -> String -> CG (SpecType, SpecType)
forall a. Maybe SrcSpan -> String -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing (String -> CG (SpecType, SpecType))
-> String -> CG (SpecType, SpecType)
forall a b. (a -> b) -> a -> b
$ String
"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, RSort)]
_ (RHole RReft
_))
  = Maybe SrcSpan -> String -> CG [FixSubC]
forall a. Maybe SrcSpan -> String -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing String
"RefTypes.rsplitC on RProp _ (RHole _)"

rsplitC CGEnv
_ (RProp [(Symbol, RSort)]
_ (RHole RReft
_)) RTProp RTyCon RTyVar RReft
_
  = Maybe SrcSpan -> String -> CG [FixSubC]
forall a. Maybe SrcSpan -> String -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing String
"RefTypes.rsplitC on RProp _ (RHole _)"

rsplitC CGEnv
γ (RProp [(Symbol, RSort)]
s1 SpecType
r1) (RProp [(Symbol, RSort)]
s2 SpecType
r2)
  = do CGEnv
γ'  <-  (CGEnv -> (String, Symbol, SpecType) -> CG CGEnv)
-> CGEnv -> [(String, Symbol, SpecType)] -> CG CGEnv
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM CGEnv -> (String, Symbol, SpecType) -> CG CGEnv
(+=) CGEnv
γ [(String
"rsplitC1", Symbol
x, RSort -> SpecType
forall r c tv. Reftable r => RType c tv () -> RType c tv r
ofRSort RSort
s) | (Symbol
x, RSort
s) <- [(Symbol, RSort)]
s2]
       SubC -> CG [FixSubC]
splitC (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,RSort
_), (Symbol
y,RSort
_)) <- [(Symbol, RSort)]
-> [(Symbol, RSort)] -> [((Symbol, RSort), (Symbol, RSort))]
forall a b. [a] -> [b] -> [(a, b)]
zip [(Symbol, RSort)]
s1 [(Symbol, RSort)]
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 RSort 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], [SpecType], [RReft], SpecType)
forallExprReftLookup CGEnv
γ Symbol
x of
      Just ([Symbol]
_,[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 RSort r,
 Reftable (RTProp RTyCon RTyVar r)) =>
TCEmb TyCon -> RRType r -> SortedReft
rTypeSortedReft (CGEnv -> TCEmb TyCon
emb CGEnv
γ) SpecType
t
      Maybe ([Symbol], [SpecType], [RReft], SpecType)
Nothing         -> Maybe Reft
forall a. Maybe a
Nothing

forallExprReft_ CGEnv
γ (F.EVar Symbol
f, [Expr]
es)
  = case CGEnv -> Symbol -> Maybe ([Symbol], [SpecType], [RReft], SpecType)
forallExprReftLookup CGEnv
γ Symbol
f of
      Just ([Symbol]
xs,[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
$ String -> [Symbol] -> [Expr] -> [(Symbol, Expr)]
forall a b.
(?callStack::CallStack) =>
String -> [a] -> [b] -> [(a, b)]
safeZip String
"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 RSort r,
 Reftable (RTProp RTyCon RTyVar r)) =>
TCEmb TyCon -> RRType r -> SortedReft
rTypeSortedReft (CGEnv -> TCEmb TyCon
emb CGEnv
γ) SpecType
t
      Maybe ([Symbol], [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], [SpecType], [RReft], SpecType)
forallExprReftLookup :: CGEnv -> Symbol -> Maybe ([Symbol], [SpecType], [RReft], SpecType)
forallExprReftLookup CGEnv
γ Symbol
x = Var -> ([Symbol], [SpecType], [RReft], SpecType)
snap (Var -> ([Symbol], [SpecType], [RReft], SpecType))
-> Maybe Var -> Maybe ([Symbol], [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
x (CGEnv -> SEnv Var
syenv CGEnv
γ)
  where
    snap :: Var -> ([Symbol], [SpecType], [RReft], SpecType)
snap     = (SpecType -> SpecType)
-> ([Symbol], [SpecType], [RReft], SpecType)
-> ([Symbol], [SpecType], [RReft], SpecType)
forall t t4 t1 t2 t3.
(t -> t4) -> (t1, t2, t3, t) -> (t1, t2, t3, t4)
mapFourth4 SpecType -> SpecType
forall t t1 t2. RType t t1 t2 -> RType t t1 t2
ignoreOblig (([Symbol], [SpecType], [RReft], SpecType)
 -> ([Symbol], [SpecType], [RReft], SpecType))
-> (Var -> ([Symbol], [SpecType], [RReft], SpecType))
-> Var
-> ([Symbol], [SpecType], [RReft], SpecType)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\(([Symbol], [SpecType], [RReft])
_,([Symbol]
a,[SpecType]
b,[RReft]
c),SpecType
t)->([Symbol]
a,[SpecType]
b,[RReft]
c,SpecType
t)) ((([Symbol], [SpecType], [RReft]), ([Symbol], [SpecType], [RReft]),
  SpecType)
 -> ([Symbol], [SpecType], [RReft], SpecType))
-> (Var
    -> (([Symbol], [SpecType], [RReft]),
        ([Symbol], [SpecType], [RReft]), SpecType))
-> Var
-> ([Symbol], [SpecType], [RReft], SpecType)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SpecType
-> (([Symbol], [SpecType], [RReft]),
    ([Symbol], [SpecType], [RReft]), SpecType)
forall t t1 a.
RType t t1 a
-> (([Symbol], [RType t t1 a], [a]),
    ([Symbol], [RType t t1 a], [a]), RType t t1 a)
bkArrow (SpecType
 -> (([Symbol], [SpecType], [RReft]),
     ([Symbol], [SpecType], [RReft]), SpecType))
-> (Var -> SpecType)
-> Var
-> (([Symbol], [SpecType], [RReft]),
    ([Symbol], [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 :: CGEnv -> x -> a
panicUnbound CGEnv
γ x
x = Error -> a
forall a e. Exception e => e -> a
Ex.throw (Error -> a) -> Error -> a
forall a b. (a -> b) -> a -> b
$ (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)