{-# LANGUAGE FlexibleInstances    #-}
{-# LANGUAGE UndecidableInstances #-}

module Language.Haskell.Liquid.Transforms.RefSplit (

        splitXRelatedRefs

        ) where

import Prelude hiding (error)

import Data.List (partition)
import Text.PrettyPrint.HughesPJ

import Language.Haskell.Liquid.Types
import Language.Haskell.Liquid.Types.PrettyPrint ()

import Language.Fixpoint.Types hiding (Predicate)
import Language.Fixpoint.Misc

splitXRelatedRefs :: Symbol -> SpecType -> (SpecType, SpecType)
splitXRelatedRefs :: Symbol -> SpecType -> (SpecType, SpecType)
splitXRelatedRefs Symbol
x SpecType
t = Symbol -> SpecType -> (SpecType, SpecType)
forall c tv.
Symbol
-> RType c tv (UReft Reft)
-> (RType c tv (UReft Reft), RType c tv (UReft Reft))
splitRType Symbol
x SpecType
t



splitRType :: Symbol
           -> RType c tv (UReft Reft)
           -> (RType c tv (UReft Reft), RType c tv (UReft Reft))
splitRType :: Symbol
-> RType c tv (UReft Reft)
-> (RType c tv (UReft Reft), RType c tv (UReft Reft))
splitRType Symbol
f (RVar tv
a UReft Reft
r) = (tv -> UReft Reft -> RType c tv (UReft Reft)
forall c tv r. tv -> r -> RType c tv r
RVar tv
a UReft Reft
r1, tv -> UReft Reft -> RType c tv (UReft Reft)
forall c tv r. tv -> r -> RType c tv r
RVar tv
a UReft Reft
r2)
  where
        (UReft Reft
r1, UReft Reft
r2) = Symbol -> UReft Reft -> (UReft Reft, UReft Reft)
splitRef Symbol
f UReft Reft
r
splitRType Symbol
f (RImpF Symbol
x RType c tv (UReft Reft)
tx RType c tv (UReft Reft)
t UReft Reft
r) = (Symbol
-> RType c tv (UReft Reft)
-> RType c tv (UReft Reft)
-> UReft Reft
-> RType c tv (UReft Reft)
forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> r -> RType c tv r
RImpF Symbol
x RType c tv (UReft Reft)
tx1 RType c tv (UReft Reft)
t1 UReft Reft
r1, Symbol
-> RType c tv (UReft Reft)
-> RType c tv (UReft Reft)
-> UReft Reft
-> RType c tv (UReft Reft)
forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> r -> RType c tv r
RImpF Symbol
x RType c tv (UReft Reft)
tx2 RType c tv (UReft Reft)
t2 UReft Reft
r2)
  where
        (RType c tv (UReft Reft)
tx1, RType c tv (UReft Reft)
tx2) = Symbol
-> RType c tv (UReft Reft)
-> (RType c tv (UReft Reft), RType c tv (UReft Reft))
forall c tv.
Symbol
-> RType c tv (UReft Reft)
-> (RType c tv (UReft Reft), RType c tv (UReft Reft))
splitRType Symbol
f RType c tv (UReft Reft)
tx
        (RType c tv (UReft Reft)
t1,  RType c tv (UReft Reft)
t2)  = Symbol
-> RType c tv (UReft Reft)
-> (RType c tv (UReft Reft), RType c tv (UReft Reft))
forall c tv.
Symbol
-> RType c tv (UReft Reft)
-> (RType c tv (UReft Reft), RType c tv (UReft Reft))
splitRType Symbol
f RType c tv (UReft Reft)
t
        (UReft Reft
r1,  UReft Reft
r2)  = Symbol -> UReft Reft -> (UReft Reft, UReft Reft)
splitRef   Symbol
f UReft Reft
r
splitRType Symbol
f (RFun Symbol
x RType c tv (UReft Reft)
tx RType c tv (UReft Reft)
t UReft Reft
r) = (Symbol
-> RType c tv (UReft Reft)
-> RType c tv (UReft Reft)
-> UReft Reft
-> RType c tv (UReft Reft)
forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
x RType c tv (UReft Reft)
tx1 RType c tv (UReft Reft)
t1 UReft Reft
r1, Symbol
-> RType c tv (UReft Reft)
-> RType c tv (UReft Reft)
-> UReft Reft
-> RType c tv (UReft Reft)
forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
x RType c tv (UReft Reft)
tx2 RType c tv (UReft Reft)
t2 UReft Reft
r2)
  where
        (RType c tv (UReft Reft)
tx1, RType c tv (UReft Reft)
tx2) = Symbol
-> RType c tv (UReft Reft)
-> (RType c tv (UReft Reft), RType c tv (UReft Reft))
forall c tv.
Symbol
-> RType c tv (UReft Reft)
-> (RType c tv (UReft Reft), RType c tv (UReft Reft))
splitRType Symbol
f RType c tv (UReft Reft)
tx
        (RType c tv (UReft Reft)
t1,  RType c tv (UReft Reft)
t2)  = Symbol
-> RType c tv (UReft Reft)
-> (RType c tv (UReft Reft), RType c tv (UReft Reft))
forall c tv.
Symbol
-> RType c tv (UReft Reft)
-> (RType c tv (UReft Reft), RType c tv (UReft Reft))
splitRType Symbol
f RType c tv (UReft Reft)
t
        (UReft Reft
r1,  UReft Reft
r2)  = Symbol -> UReft Reft -> (UReft Reft, UReft Reft)
splitRef   Symbol
f UReft Reft
r
splitRType Symbol
f (RAllT RTVU c tv
v RType c tv (UReft Reft)
t UReft Reft
r) = (RTVU c tv
-> RType c tv (UReft Reft) -> UReft Reft -> RType c tv (UReft Reft)
forall c tv r. RTVU c tv -> RType c tv r -> r -> RType c tv r
RAllT RTVU c tv
v RType c tv (UReft Reft)
t1 UReft Reft
r1, RTVU c tv
-> RType c tv (UReft Reft) -> UReft Reft -> RType c tv (UReft Reft)
forall c tv r. RTVU c tv -> RType c tv r -> r -> RType c tv r
RAllT RTVU c tv
v RType c tv (UReft Reft)
t2 UReft Reft
r2)
  where
        (RType c tv (UReft Reft)
t1, RType c tv (UReft Reft)
t2) = Symbol
-> RType c tv (UReft Reft)
-> (RType c tv (UReft Reft), RType c tv (UReft Reft))
forall c tv.
Symbol
-> RType c tv (UReft Reft)
-> (RType c tv (UReft Reft), RType c tv (UReft Reft))
splitRType Symbol
f RType c tv (UReft Reft)
t
        (UReft Reft
r1,  UReft Reft
r2)  = Symbol -> UReft Reft -> (UReft Reft, UReft Reft)
splitRef   Symbol
f UReft Reft
r
splitRType Symbol
f (RAllP PVU c tv
p RType c tv (UReft Reft)
t) = (PVU c tv -> RType c tv (UReft Reft) -> RType c tv (UReft Reft)
forall c tv r. PVU c tv -> RType c tv r -> RType c tv r
RAllP PVU c tv
p RType c tv (UReft Reft)
t1, PVU c tv -> RType c tv (UReft Reft) -> RType c tv (UReft Reft)
forall c tv r. PVU c tv -> RType c tv r -> RType c tv r
RAllP PVU c tv
p RType c tv (UReft Reft)
t2)
  where
        (RType c tv (UReft Reft)
t1, RType c tv (UReft Reft)
t2) = Symbol
-> RType c tv (UReft Reft)
-> (RType c tv (UReft Reft), RType c tv (UReft Reft))
forall c tv.
Symbol
-> RType c tv (UReft Reft)
-> (RType c tv (UReft Reft), RType c tv (UReft Reft))
splitRType Symbol
f RType c tv (UReft Reft)
t
splitRType Symbol
f (RApp c
c [RType c tv (UReft Reft)]
ts [RTProp c tv (UReft Reft)]
rs UReft Reft
r) = (c
-> [RType c tv (UReft Reft)]
-> [RTProp c tv (UReft Reft)]
-> UReft Reft
-> RType c tv (UReft Reft)
forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp c
c [RType c tv (UReft Reft)]
ts1 [RTProp c tv (UReft Reft)]
rs1 UReft Reft
r1, c
-> [RType c tv (UReft Reft)]
-> [RTProp c tv (UReft Reft)]
-> UReft Reft
-> RType c tv (UReft Reft)
forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp c
c [RType c tv (UReft Reft)]
ts2 [RTProp c tv (UReft Reft)]
rs2 UReft Reft
r2)
  where
        ([RType c tv (UReft Reft)]
ts1, [RType c tv (UReft Reft)]
ts2) = [(RType c tv (UReft Reft), RType c tv (UReft Reft))]
-> ([RType c tv (UReft Reft)], [RType c tv (UReft Reft)])
forall a b. [(a, b)] -> ([a], [b])
unzip (Symbol
-> RType c tv (UReft Reft)
-> (RType c tv (UReft Reft), RType c tv (UReft Reft))
forall c tv.
Symbol
-> RType c tv (UReft Reft)
-> (RType c tv (UReft Reft), RType c tv (UReft Reft))
splitRType Symbol
f (RType c tv (UReft Reft)
 -> (RType c tv (UReft Reft), RType c tv (UReft Reft)))
-> [RType c tv (UReft Reft)]
-> [(RType c tv (UReft Reft), RType c tv (UReft Reft))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RType c tv (UReft Reft)]
ts)
        ([RTProp c tv (UReft Reft)]
rs1, [RTProp c tv (UReft Reft)]
rs2) = [(RTProp c tv (UReft Reft), RTProp c tv (UReft Reft))]
-> ([RTProp c tv (UReft Reft)], [RTProp c tv (UReft Reft)])
forall a b. [(a, b)] -> ([a], [b])
unzip (Symbol
-> RTProp c tv (UReft Reft)
-> (RTProp c tv (UReft Reft), RTProp c tv (UReft Reft))
forall c tv.
Symbol
-> RTProp c tv (UReft Reft)
-> (RTProp c tv (UReft Reft), RTProp c tv (UReft Reft))
splitUReft Symbol
f (RTProp c tv (UReft Reft)
 -> (RTProp c tv (UReft Reft), RTProp c tv (UReft Reft)))
-> [RTProp c tv (UReft Reft)]
-> [(RTProp c tv (UReft Reft), RTProp c tv (UReft Reft))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RTProp c tv (UReft Reft)]
rs)
        (UReft Reft
r1,  UReft Reft
r2)  = Symbol -> UReft Reft -> (UReft Reft, UReft Reft)
splitRef Symbol
f UReft Reft
r
splitRType Symbol
f (RAllE Symbol
x RType c tv (UReft Reft)
tx RType c tv (UReft Reft)
t) = (Symbol
-> RType c tv (UReft Reft)
-> RType c tv (UReft Reft)
-> RType c tv (UReft Reft)
forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> RType c tv r
RAllE Symbol
x RType c tv (UReft Reft)
tx1 RType c tv (UReft Reft)
t1, Symbol
-> RType c tv (UReft Reft)
-> RType c tv (UReft Reft)
-> RType c tv (UReft Reft)
forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> RType c tv r
RAllE Symbol
x RType c tv (UReft Reft)
tx2 RType c tv (UReft Reft)
t2)
  where
        (RType c tv (UReft Reft)
tx1, RType c tv (UReft Reft)
tx2) = Symbol
-> RType c tv (UReft Reft)
-> (RType c tv (UReft Reft), RType c tv (UReft Reft))
forall c tv.
Symbol
-> RType c tv (UReft Reft)
-> (RType c tv (UReft Reft), RType c tv (UReft Reft))
splitRType Symbol
f RType c tv (UReft Reft)
tx
        (RType c tv (UReft Reft)
t1, RType c tv (UReft Reft)
t2)   = Symbol
-> RType c tv (UReft Reft)
-> (RType c tv (UReft Reft), RType c tv (UReft Reft))
forall c tv.
Symbol
-> RType c tv (UReft Reft)
-> (RType c tv (UReft Reft), RType c tv (UReft Reft))
splitRType Symbol
f RType c tv (UReft Reft)
t
splitRType Symbol
f (REx Symbol
x RType c tv (UReft Reft)
tx RType c tv (UReft Reft)
t) = (Symbol
-> RType c tv (UReft Reft)
-> RType c tv (UReft Reft)
-> RType c tv (UReft Reft)
forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> RType c tv r
REx Symbol
x RType c tv (UReft Reft)
tx1 RType c tv (UReft Reft)
t1, Symbol
-> RType c tv (UReft Reft)
-> RType c tv (UReft Reft)
-> RType c tv (UReft Reft)
forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> RType c tv r
REx Symbol
x RType c tv (UReft Reft)
tx2 RType c tv (UReft Reft)
t2)
  where
        (RType c tv (UReft Reft)
tx1, RType c tv (UReft Reft)
tx2) = Symbol
-> RType c tv (UReft Reft)
-> (RType c tv (UReft Reft), RType c tv (UReft Reft))
forall c tv.
Symbol
-> RType c tv (UReft Reft)
-> (RType c tv (UReft Reft), RType c tv (UReft Reft))
splitRType Symbol
f RType c tv (UReft Reft)
tx
        (RType c tv (UReft Reft)
t1, RType c tv (UReft Reft)
t2)   = Symbol
-> RType c tv (UReft Reft)
-> (RType c tv (UReft Reft), RType c tv (UReft Reft))
forall c tv.
Symbol
-> RType c tv (UReft Reft)
-> (RType c tv (UReft Reft), RType c tv (UReft Reft))
splitRType Symbol
f RType c tv (UReft Reft)
t
splitRType Symbol
_ (RExprArg Located Expr
e) = (Located Expr -> RType c tv (UReft Reft)
forall c tv r. Located Expr -> RType c tv r
RExprArg Located Expr
e, Located Expr -> RType c tv (UReft Reft)
forall c tv r. Located Expr -> RType c tv r
RExprArg Located Expr
e)
splitRType Symbol
f (RAppTy RType c tv (UReft Reft)
tx RType c tv (UReft Reft)
t UReft Reft
r) = (RType c tv (UReft Reft)
-> RType c tv (UReft Reft) -> UReft Reft -> RType c tv (UReft Reft)
forall c tv r. RType c tv r -> RType c tv r -> r -> RType c tv r
RAppTy RType c tv (UReft Reft)
tx1 RType c tv (UReft Reft)
t1 UReft Reft
r1, RType c tv (UReft Reft)
-> RType c tv (UReft Reft) -> UReft Reft -> RType c tv (UReft Reft)
forall c tv r. RType c tv r -> RType c tv r -> r -> RType c tv r
RAppTy RType c tv (UReft Reft)
tx2 RType c tv (UReft Reft)
t2 UReft Reft
r2)
  where
        (RType c tv (UReft Reft)
tx1, RType c tv (UReft Reft)
tx2) = Symbol
-> RType c tv (UReft Reft)
-> (RType c tv (UReft Reft), RType c tv (UReft Reft))
forall c tv.
Symbol
-> RType c tv (UReft Reft)
-> (RType c tv (UReft Reft), RType c tv (UReft Reft))
splitRType Symbol
f RType c tv (UReft Reft)
tx
        (RType c tv (UReft Reft)
t1,  RType c tv (UReft Reft)
t2)  = Symbol
-> RType c tv (UReft Reft)
-> (RType c tv (UReft Reft), RType c tv (UReft Reft))
forall c tv.
Symbol
-> RType c tv (UReft Reft)
-> (RType c tv (UReft Reft), RType c tv (UReft Reft))
splitRType Symbol
f RType c tv (UReft Reft)
t
        (UReft Reft
r1,  UReft Reft
r2)  = Symbol -> UReft Reft -> (UReft Reft, UReft Reft)
splitRef   Symbol
f UReft Reft
r
splitRType Symbol
f (RRTy [(Symbol, RType c tv (UReft Reft))]
xs UReft Reft
r Oblig
o RType c tv (UReft Reft)
t) = ([(Symbol, RType c tv (UReft Reft))]
-> UReft Reft
-> Oblig
-> RType c tv (UReft Reft)
-> RType c tv (UReft Reft)
forall c tv r.
[(Symbol, RType c tv r)]
-> r -> Oblig -> RType c tv r -> RType c tv r
RRTy [(Symbol, RType c tv (UReft Reft))]
xs1 UReft Reft
r1 Oblig
o RType c tv (UReft Reft)
t1, [(Symbol, RType c tv (UReft Reft))]
-> UReft Reft
-> Oblig
-> RType c tv (UReft Reft)
-> RType c tv (UReft Reft)
forall c tv r.
[(Symbol, RType c tv r)]
-> r -> Oblig -> RType c tv r -> RType c tv r
RRTy [(Symbol, RType c tv (UReft Reft))]
xs2 UReft Reft
r2 Oblig
o RType c tv (UReft Reft)
t2)
  where
        ([(Symbol, RType c tv (UReft Reft))]
xs1, [(Symbol, RType c tv (UReft Reft))]
xs2) = [((Symbol, RType c tv (UReft Reft)),
  (Symbol, RType c tv (UReft Reft)))]
-> ([(Symbol, RType c tv (UReft Reft))],
    [(Symbol, RType c tv (UReft Reft))])
forall a b. [(a, b)] -> ([a], [b])
unzip ((Symbol, RType c tv (UReft Reft))
-> ((Symbol, RType c tv (UReft Reft)),
    (Symbol, RType c tv (UReft Reft)))
forall a c tv.
(a, RType c tv (UReft Reft))
-> ((a, RType c tv (UReft Reft)), (a, RType c tv (UReft Reft)))
go ((Symbol, RType c tv (UReft Reft))
 -> ((Symbol, RType c tv (UReft Reft)),
     (Symbol, RType c tv (UReft Reft))))
-> [(Symbol, RType c tv (UReft Reft))]
-> [((Symbol, RType c tv (UReft Reft)),
     (Symbol, RType c tv (UReft Reft)))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, RType c tv (UReft Reft))]
xs)
        (UReft Reft
r1, UReft Reft
r2) = Symbol -> UReft Reft -> (UReft Reft, UReft Reft)
splitRef   Symbol
f UReft Reft
r
        (RType c tv (UReft Reft)
t1, RType c tv (UReft Reft)
t2) = Symbol
-> RType c tv (UReft Reft)
-> (RType c tv (UReft Reft), RType c tv (UReft Reft))
forall c tv.
Symbol
-> RType c tv (UReft Reft)
-> (RType c tv (UReft Reft), RType c tv (UReft Reft))
splitRType Symbol
f RType c tv (UReft Reft)
t

        go :: (a, RType c tv (UReft Reft))
-> ((a, RType c tv (UReft Reft)), (a, RType c tv (UReft Reft)))
go (a
x, RType c tv (UReft Reft)
t) = let (RType c tv (UReft Reft)
t1, RType c tv (UReft Reft)
t2) = Symbol
-> RType c tv (UReft Reft)
-> (RType c tv (UReft Reft), RType c tv (UReft Reft))
forall c tv.
Symbol
-> RType c tv (UReft Reft)
-> (RType c tv (UReft Reft), RType c tv (UReft Reft))
splitRType Symbol
f RType c tv (UReft Reft)
t in ((a
x,RType c tv (UReft Reft)
t1), (a
x, RType c tv (UReft Reft)
t2))
splitRType Symbol
f (RHole UReft Reft
r) = (UReft Reft -> RType c tv (UReft Reft)
forall c tv r. r -> RType c tv r
RHole UReft Reft
r1, UReft Reft -> RType c tv (UReft Reft)
forall c tv r. r -> RType c tv r
RHole UReft Reft
r2)
  where
        (UReft Reft
r1, UReft Reft
r2) = Symbol -> UReft Reft -> (UReft Reft, UReft Reft)
splitRef Symbol
f UReft Reft
r


splitUReft :: Symbol -> RTProp c tv (UReft Reft) -> (RTProp c tv (UReft Reft), RTProp c tv (UReft Reft))
splitUReft :: Symbol
-> RTProp c tv (UReft Reft)
-> (RTProp c tv (UReft Reft), RTProp c tv (UReft Reft))
splitUReft Symbol
x (RProp [(Symbol, RType c tv ())]
xs (RHole UReft Reft
r)) = ([(Symbol, RType c tv ())]
-> RType c tv (UReft Reft) -> RTProp c tv (UReft Reft)
forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp [(Symbol, RType c tv ())]
xs (UReft Reft -> RType c tv (UReft Reft)
forall c tv r. r -> RType c tv r
RHole UReft Reft
r1), [(Symbol, RType c tv ())]
-> RType c tv (UReft Reft) -> RTProp c tv (UReft Reft)
forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp [(Symbol, RType c tv ())]
xs (UReft Reft -> RType c tv (UReft Reft)
forall c tv r. r -> RType c tv r
RHole UReft Reft
r2))
  where
        (UReft Reft
r1, UReft Reft
r2) = Symbol -> UReft Reft -> (UReft Reft, UReft Reft)
splitRef Symbol
x UReft Reft
r
splitUReft Symbol
x (RProp [(Symbol, RType c tv ())]
xs RType c tv (UReft Reft)
t) = ([(Symbol, RType c tv ())]
-> RType c tv (UReft Reft) -> RTProp c tv (UReft Reft)
forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp [(Symbol, RType c tv ())]
xs RType c tv (UReft Reft)
t1, [(Symbol, RType c tv ())]
-> RType c tv (UReft Reft) -> RTProp c tv (UReft Reft)
forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp [(Symbol, RType c tv ())]
xs RType c tv (UReft Reft)
t2)
  where
        (RType c tv (UReft Reft)
t1, RType c tv (UReft Reft)
t2) = Symbol
-> RType c tv (UReft Reft)
-> (RType c tv (UReft Reft), RType c tv (UReft Reft))
forall c tv.
Symbol
-> RType c tv (UReft Reft)
-> (RType c tv (UReft Reft), RType c tv (UReft Reft))
splitRType Symbol
x RType c tv (UReft Reft)
t

splitRef :: Symbol -> UReft Reft -> (UReft Reft, UReft Reft)
splitRef :: Symbol -> UReft Reft -> (UReft Reft, UReft Reft)
splitRef Symbol
f (MkUReft Reft
r Predicate
p) = (Reft -> Predicate -> UReft Reft
forall r. r -> Predicate -> UReft r
MkUReft Reft
r1 Predicate
p1, Reft -> Predicate -> UReft Reft
forall r. r -> Predicate -> UReft r
MkUReft Reft
r2 Predicate
p2)
        where
                (Reft
r1, Reft
r2) = Symbol -> Reft -> (Reft, Reft)
splitReft Symbol
f Reft
r
                (Predicate
p1, Predicate
p2) = Symbol -> Predicate -> (Predicate, Predicate)
splitPred Symbol
f Predicate
p

splitReft :: Symbol -> Reft -> (Reft, Reft)
splitReft :: Symbol -> Reft -> (Reft, Reft)
splitReft Symbol
f (Reft (Symbol
v, Expr
xs)) = ((Symbol, Expr) -> Reft
Reft (Symbol
v, ListNE Expr -> Expr
pAnd ListNE Expr
xs1), (Symbol, Expr) -> Reft
Reft (Symbol
v, ListNE Expr -> Expr
pAnd ListNE Expr
xs2))
  where
    (ListNE Expr
xs1, ListNE Expr
xs2)       = (Expr -> Bool) -> ListNE Expr -> (ListNE Expr, ListNE Expr)
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (Symbol -> Expr -> Bool
forall a. IsFree a => Symbol -> a -> Bool
isFree Symbol
f) (Expr -> ListNE Expr
unPAnd Expr
xs)

    unPAnd :: Expr -> ListNE Expr
unPAnd (PAnd ListNE Expr
ps) = (Expr -> ListNE Expr) -> ListNE Expr -> ListNE Expr
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Expr -> ListNE Expr
unPAnd ListNE Expr
ps
    unPAnd Expr
p         = [Expr
p]


splitPred :: Symbol -> Predicate -> (Predicate, Predicate)
splitPred :: Symbol -> Predicate -> (Predicate, Predicate)
splitPred Symbol
f (Pr [UsedPVar]
ps) = ([UsedPVar] -> Predicate
Pr [UsedPVar]
ps1, [UsedPVar] -> Predicate
Pr [UsedPVar]
ps2)
  where
    ([UsedPVar]
ps1, [UsedPVar]
ps2) = (UsedPVar -> Bool) -> [UsedPVar] -> ([UsedPVar], [UsedPVar])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition UsedPVar -> Bool
forall a. PVar a -> Bool
g [UsedPVar]
ps
    g :: PVar a -> Bool
g PVar a
p = (Expr -> Bool) -> ListNE Expr -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Symbol -> Expr -> Bool
forall a. IsFree a => Symbol -> a -> Bool
isFree Symbol
f) ((a, Symbol, Expr) -> Expr
forall a b c. (a, b, c) -> c
thd3 ((a, Symbol, Expr) -> Expr) -> [(a, Symbol, Expr)] -> ListNE Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PVar a -> [(a, Symbol, Expr)]
forall t. PVar t -> [(t, Symbol, Expr)]
pargs PVar a
p)


class IsFree a where
        isFree :: Symbol -> a -> Bool

instance (Subable x) => (IsFree x) where
        isFree :: Symbol -> x -> Bool
isFree Symbol
x x
p = Symbol
x Symbol -> [Symbol] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` x -> [Symbol]
forall a. Subable a => a -> [Symbol]
syms x
p

instance Show (UReft Reft) where
         show :: UReft Reft -> String
show = Doc -> String
render (Doc -> String) -> (UReft Reft -> Doc) -> UReft Reft -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UReft Reft -> Doc
forall a. PPrint a => a -> Doc
pprint