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

{-# OPTIONS_GHC -Wno-orphans #-}

module Language.Haskell.Liquid.Transforms.RefSplit (

        splitXRelatedRefs

        ) where

import Prelude hiding (error)

import Data.List (partition)

import Language.Haskell.Liquid.Types.RType
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 :: forall c tv.
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 -> RTypeV Symbol c tv (UReft Reft)
forall v c tv r. tv -> r -> RTypeV v c tv r
RVar tv
a UReft Reft
r1, tv -> UReft Reft -> RTypeV Symbol c tv (UReft Reft)
forall v c tv r. tv -> r -> RTypeV v 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 (RFun Symbol
x RFInfo
i RTypeV Symbol c tv (UReft Reft)
tx RTypeV Symbol c tv (UReft Reft)
t UReft Reft
r) = (Symbol
-> RFInfo
-> RTypeV Symbol c tv (UReft Reft)
-> RTypeV Symbol c tv (UReft Reft)
-> UReft Reft
-> RTypeV Symbol c tv (UReft Reft)
forall v c tv r.
Symbol
-> RFInfo
-> RTypeV v c tv r
-> RTypeV v c tv r
-> r
-> RTypeV v c tv r
RFun Symbol
x RFInfo
i RTypeV Symbol c tv (UReft Reft)
tx1 RTypeV Symbol c tv (UReft Reft)
t1 UReft Reft
r1, Symbol
-> RFInfo
-> RTypeV Symbol c tv (UReft Reft)
-> RTypeV Symbol c tv (UReft Reft)
-> UReft Reft
-> RTypeV Symbol c tv (UReft Reft)
forall v c tv r.
Symbol
-> RFInfo
-> RTypeV v c tv r
-> RTypeV v c tv r
-> r
-> RTypeV v c tv r
RFun Symbol
x RFInfo
i RTypeV Symbol c tv (UReft Reft)
tx2 RTypeV Symbol c tv (UReft Reft)
t2 UReft Reft
r2)
  where
        (RTypeV Symbol c tv (UReft Reft)
tx1, RTypeV Symbol c tv (UReft Reft)
tx2) = Symbol
-> RTypeV Symbol c tv (UReft Reft)
-> (RTypeV Symbol c tv (UReft Reft),
    RTypeV Symbol 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 RTypeV Symbol c tv (UReft Reft)
tx
        (RTypeV Symbol c tv (UReft Reft)
t1,  RTypeV Symbol c tv (UReft Reft)
t2)  = Symbol
-> RTypeV Symbol c tv (UReft Reft)
-> (RTypeV Symbol c tv (UReft Reft),
    RTypeV Symbol 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 RTypeV Symbol 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 RTVUV Symbol c tv
v RTypeV Symbol c tv (UReft Reft)
t UReft Reft
r) = (RTVUV Symbol c tv
-> RTypeV Symbol c tv (UReft Reft)
-> UReft Reft
-> RTypeV Symbol c tv (UReft Reft)
forall v c tv r.
RTVUV v c tv -> RTypeV v c tv r -> r -> RTypeV v c tv r
RAllT RTVUV Symbol c tv
v RTypeV Symbol c tv (UReft Reft)
t1 UReft Reft
r1, RTVUV Symbol c tv
-> RTypeV Symbol c tv (UReft Reft)
-> UReft Reft
-> RTypeV Symbol c tv (UReft Reft)
forall v c tv r.
RTVUV v c tv -> RTypeV v c tv r -> r -> RTypeV v c tv r
RAllT RTVUV Symbol c tv
v RTypeV Symbol c tv (UReft Reft)
t2 UReft Reft
r2)
  where
        (RTypeV Symbol c tv (UReft Reft)
t1, RTypeV Symbol c tv (UReft Reft)
t2) = Symbol
-> RTypeV Symbol c tv (UReft Reft)
-> (RTypeV Symbol c tv (UReft Reft),
    RTypeV Symbol 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 RTypeV Symbol 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 PVUV Symbol c tv
p RTypeV Symbol c tv (UReft Reft)
t) = (PVUV Symbol c tv
-> RTypeV Symbol c tv (UReft Reft)
-> RTypeV Symbol c tv (UReft Reft)
forall v c tv r. PVUV v c tv -> RTypeV v c tv r -> RTypeV v c tv r
RAllP PVUV Symbol c tv
p RTypeV Symbol c tv (UReft Reft)
t1, PVUV Symbol c tv
-> RTypeV Symbol c tv (UReft Reft)
-> RTypeV Symbol c tv (UReft Reft)
forall v c tv r. PVUV v c tv -> RTypeV v c tv r -> RTypeV v c tv r
RAllP PVUV Symbol c tv
p RTypeV Symbol c tv (UReft Reft)
t2)
  where
        (RTypeV Symbol c tv (UReft Reft)
t1, RTypeV Symbol c tv (UReft Reft)
t2) = Symbol
-> RTypeV Symbol c tv (UReft Reft)
-> (RTypeV Symbol c tv (UReft Reft),
    RTypeV Symbol 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 RTypeV Symbol c tv (UReft Reft)
t
splitRType Symbol
f (RApp c
c [RTypeV Symbol c tv (UReft Reft)]
ts [RTPropV Symbol c tv (UReft Reft)]
rs UReft Reft
r) = (c
-> [RTypeV Symbol c tv (UReft Reft)]
-> [RTPropV Symbol c tv (UReft Reft)]
-> UReft Reft
-> RTypeV Symbol c tv (UReft Reft)
forall v c tv r.
c
-> [RTypeV v c tv r] -> [RTPropV v c tv r] -> r -> RTypeV v c tv r
RApp c
c [RTypeV Symbol c tv (UReft Reft)]
ts1 [RTPropV Symbol c tv (UReft Reft)]
rs1 UReft Reft
r1, c
-> [RTypeV Symbol c tv (UReft Reft)]
-> [RTPropV Symbol c tv (UReft Reft)]
-> UReft Reft
-> RTypeV Symbol c tv (UReft Reft)
forall v c tv r.
c
-> [RTypeV v c tv r] -> [RTPropV v c tv r] -> r -> RTypeV v c tv r
RApp c
c [RTypeV Symbol c tv (UReft Reft)]
ts2 [RTPropV Symbol c tv (UReft Reft)]
rs2 UReft Reft
r2)
  where
        ([RTypeV Symbol c tv (UReft Reft)]
ts1, [RTypeV Symbol c tv (UReft Reft)]
ts2) = [(RTypeV Symbol c tv (UReft Reft),
  RTypeV Symbol c tv (UReft Reft))]
-> ([RTypeV Symbol c tv (UReft Reft)],
    [RTypeV Symbol c tv (UReft Reft)])
forall a b. [(a, b)] -> ([a], [b])
unzip (Symbol
-> RTypeV Symbol c tv (UReft Reft)
-> (RTypeV Symbol c tv (UReft Reft),
    RTypeV Symbol 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 (RTypeV Symbol c tv (UReft Reft)
 -> (RTypeV Symbol c tv (UReft Reft),
     RTypeV Symbol c tv (UReft Reft)))
-> [RTypeV Symbol c tv (UReft Reft)]
-> [(RTypeV Symbol c tv (UReft Reft),
     RTypeV Symbol c tv (UReft Reft))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RTypeV Symbol c tv (UReft Reft)]
ts)
        ([RTPropV Symbol c tv (UReft Reft)]
rs1, [RTPropV Symbol c tv (UReft Reft)]
rs2) = [(RTPropV Symbol c tv (UReft Reft),
  RTPropV Symbol c tv (UReft Reft))]
-> ([RTPropV Symbol c tv (UReft Reft)],
    [RTPropV Symbol c tv (UReft Reft)])
forall a b. [(a, b)] -> ([a], [b])
unzip (Symbol
-> RTPropV Symbol c tv (UReft Reft)
-> (RTPropV Symbol c tv (UReft Reft),
    RTPropV Symbol 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 (RTPropV Symbol c tv (UReft Reft)
 -> (RTPropV Symbol c tv (UReft Reft),
     RTPropV Symbol c tv (UReft Reft)))
-> [RTPropV Symbol c tv (UReft Reft)]
-> [(RTPropV Symbol c tv (UReft Reft),
     RTPropV Symbol c tv (UReft Reft))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RTPropV Symbol 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 RTypeV Symbol c tv (UReft Reft)
tx RTypeV Symbol c tv (UReft Reft)
t) = (Symbol
-> RTypeV Symbol c tv (UReft Reft)
-> RTypeV Symbol c tv (UReft Reft)
-> RTypeV Symbol c tv (UReft Reft)
forall v c tv r.
Symbol -> RTypeV v c tv r -> RTypeV v c tv r -> RTypeV v c tv r
RAllE Symbol
x RTypeV Symbol c tv (UReft Reft)
tx1 RTypeV Symbol c tv (UReft Reft)
t1, Symbol
-> RTypeV Symbol c tv (UReft Reft)
-> RTypeV Symbol c tv (UReft Reft)
-> RTypeV Symbol c tv (UReft Reft)
forall v c tv r.
Symbol -> RTypeV v c tv r -> RTypeV v c tv r -> RTypeV v c tv r
RAllE Symbol
x RTypeV Symbol c tv (UReft Reft)
tx2 RTypeV Symbol c tv (UReft Reft)
t2)
  where
        (RTypeV Symbol c tv (UReft Reft)
tx1, RTypeV Symbol c tv (UReft Reft)
tx2) = Symbol
-> RTypeV Symbol c tv (UReft Reft)
-> (RTypeV Symbol c tv (UReft Reft),
    RTypeV Symbol 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 RTypeV Symbol c tv (UReft Reft)
tx
        (RTypeV Symbol c tv (UReft Reft)
t1, RTypeV Symbol c tv (UReft Reft)
t2)   = Symbol
-> RTypeV Symbol c tv (UReft Reft)
-> (RTypeV Symbol c tv (UReft Reft),
    RTypeV Symbol 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 RTypeV Symbol c tv (UReft Reft)
t
splitRType Symbol
f (REx Symbol
x RTypeV Symbol c tv (UReft Reft)
tx RTypeV Symbol c tv (UReft Reft)
t) = (Symbol
-> RTypeV Symbol c tv (UReft Reft)
-> RTypeV Symbol c tv (UReft Reft)
-> RTypeV Symbol c tv (UReft Reft)
forall v c tv r.
Symbol -> RTypeV v c tv r -> RTypeV v c tv r -> RTypeV v c tv r
REx Symbol
x RTypeV Symbol c tv (UReft Reft)
tx1 RTypeV Symbol c tv (UReft Reft)
t1, Symbol
-> RTypeV Symbol c tv (UReft Reft)
-> RTypeV Symbol c tv (UReft Reft)
-> RTypeV Symbol c tv (UReft Reft)
forall v c tv r.
Symbol -> RTypeV v c tv r -> RTypeV v c tv r -> RTypeV v c tv r
REx Symbol
x RTypeV Symbol c tv (UReft Reft)
tx2 RTypeV Symbol c tv (UReft Reft)
t2)
  where
        (RTypeV Symbol c tv (UReft Reft)
tx1, RTypeV Symbol c tv (UReft Reft)
tx2) = Symbol
-> RTypeV Symbol c tv (UReft Reft)
-> (RTypeV Symbol c tv (UReft Reft),
    RTypeV Symbol 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 RTypeV Symbol c tv (UReft Reft)
tx
        (RTypeV Symbol c tv (UReft Reft)
t1, RTypeV Symbol c tv (UReft Reft)
t2)   = Symbol
-> RTypeV Symbol c tv (UReft Reft)
-> (RTypeV Symbol c tv (UReft Reft),
    RTypeV Symbol 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 RTypeV Symbol c tv (UReft Reft)
t
splitRType Symbol
_ (RExprArg Located (ExprV Symbol)
e) = (Located (ExprV Symbol) -> RTypeV Symbol c tv (UReft Reft)
forall v c tv r. Located (ExprV v) -> RTypeV v c tv r
RExprArg Located (ExprV Symbol)
e, Located (ExprV Symbol) -> RTypeV Symbol c tv (UReft Reft)
forall v c tv r. Located (ExprV v) -> RTypeV v c tv r
RExprArg Located (ExprV Symbol)
e)
splitRType Symbol
f (RAppTy RTypeV Symbol c tv (UReft Reft)
tx RTypeV Symbol c tv (UReft Reft)
t UReft Reft
r) = (RTypeV Symbol c tv (UReft Reft)
-> RTypeV Symbol c tv (UReft Reft)
-> UReft Reft
-> RTypeV Symbol c tv (UReft Reft)
forall v c tv r.
RTypeV v c tv r -> RTypeV v c tv r -> r -> RTypeV v c tv r
RAppTy RTypeV Symbol c tv (UReft Reft)
tx1 RTypeV Symbol c tv (UReft Reft)
t1 UReft Reft
r1, RTypeV Symbol c tv (UReft Reft)
-> RTypeV Symbol c tv (UReft Reft)
-> UReft Reft
-> RTypeV Symbol c tv (UReft Reft)
forall v c tv r.
RTypeV v c tv r -> RTypeV v c tv r -> r -> RTypeV v c tv r
RAppTy RTypeV Symbol c tv (UReft Reft)
tx2 RTypeV Symbol c tv (UReft Reft)
t2 UReft Reft
r2)
  where
        (RTypeV Symbol c tv (UReft Reft)
tx1, RTypeV Symbol c tv (UReft Reft)
tx2) = Symbol
-> RTypeV Symbol c tv (UReft Reft)
-> (RTypeV Symbol c tv (UReft Reft),
    RTypeV Symbol 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 RTypeV Symbol c tv (UReft Reft)
tx
        (RTypeV Symbol c tv (UReft Reft)
t1,  RTypeV Symbol c tv (UReft Reft)
t2)  = Symbol
-> RTypeV Symbol c tv (UReft Reft)
-> (RTypeV Symbol c tv (UReft Reft),
    RTypeV Symbol 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 RTypeV Symbol 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, RTypeV Symbol c tv (UReft Reft))]
xs UReft Reft
r Oblig
o RTypeV Symbol c tv (UReft Reft)
rt) = ([(Symbol, RTypeV Symbol c tv (UReft Reft))]
-> UReft Reft
-> Oblig
-> RTypeV Symbol c tv (UReft Reft)
-> RTypeV Symbol c tv (UReft Reft)
forall v c tv r.
[(Symbol, RTypeV v c tv r)]
-> r -> Oblig -> RTypeV v c tv r -> RTypeV v c tv r
RRTy [(Symbol, RTypeV Symbol c tv (UReft Reft))]
xs1 UReft Reft
r1 Oblig
o RTypeV Symbol c tv (UReft Reft)
rt1, [(Symbol, RTypeV Symbol c tv (UReft Reft))]
-> UReft Reft
-> Oblig
-> RTypeV Symbol c tv (UReft Reft)
-> RTypeV Symbol c tv (UReft Reft)
forall v c tv r.
[(Symbol, RTypeV v c tv r)]
-> r -> Oblig -> RTypeV v c tv r -> RTypeV v c tv r
RRTy [(Symbol, RTypeV Symbol c tv (UReft Reft))]
xs2 UReft Reft
r2 Oblig
o RTypeV Symbol c tv (UReft Reft)
rt2)
  where
        ([(Symbol, RTypeV Symbol c tv (UReft Reft))]
xs1, [(Symbol, RTypeV Symbol c tv (UReft Reft))]
xs2) = [((Symbol, RTypeV Symbol c tv (UReft Reft)),
  (Symbol, RTypeV Symbol c tv (UReft Reft)))]
-> ([(Symbol, RTypeV Symbol c tv (UReft Reft))],
    [(Symbol, RTypeV Symbol c tv (UReft Reft))])
forall a b. [(a, b)] -> ([a], [b])
unzip ((Symbol, RTypeV Symbol c tv (UReft Reft))
-> ((Symbol, RTypeV Symbol c tv (UReft Reft)),
    (Symbol, RTypeV Symbol 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, RTypeV Symbol c tv (UReft Reft))
 -> ((Symbol, RTypeV Symbol c tv (UReft Reft)),
     (Symbol, RTypeV Symbol c tv (UReft Reft))))
-> [(Symbol, RTypeV Symbol c tv (UReft Reft))]
-> [((Symbol, RTypeV Symbol c tv (UReft Reft)),
     (Symbol, RTypeV Symbol c tv (UReft Reft)))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, RTypeV Symbol c tv (UReft Reft))]
xs)
        (UReft Reft
r1, UReft Reft
r2) = Symbol -> UReft Reft -> (UReft Reft, UReft Reft)
splitRef   Symbol
f UReft Reft
r
        (RTypeV Symbol c tv (UReft Reft)
rt1, RTypeV Symbol c tv (UReft Reft)
rt2) = Symbol
-> RTypeV Symbol c tv (UReft Reft)
-> (RTypeV Symbol c tv (UReft Reft),
    RTypeV Symbol 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 RTypeV Symbol c tv (UReft Reft)
rt

        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 -> RTypeV Symbol c tv (UReft Reft)
forall v c tv r. r -> RTypeV v c tv r
RHole UReft Reft
r1, UReft Reft -> RTypeV Symbol c tv (UReft Reft)
forall v c tv r. r -> RTypeV v 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 :: forall c tv.
Symbol
-> RTProp c tv (UReft Reft)
-> (RTProp c tv (UReft Reft), RTProp c tv (UReft Reft))
splitUReft Symbol
x (RProp [(Symbol, RTypeV Symbol c tv ())]
xs (RHole UReft Reft
r)) = ([(Symbol, RTypeV Symbol c tv ())]
-> RTypeV Symbol c tv (UReft Reft)
-> Ref (RTypeV Symbol c tv ()) (RTypeV Symbol c tv (UReft Reft))
forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp [(Symbol, RTypeV Symbol c tv ())]
xs (UReft Reft -> RTypeV Symbol c tv (UReft Reft)
forall v c tv r. r -> RTypeV v c tv r
RHole UReft Reft
r1), [(Symbol, RTypeV Symbol c tv ())]
-> RTypeV Symbol c tv (UReft Reft)
-> Ref (RTypeV Symbol c tv ()) (RTypeV Symbol c tv (UReft Reft))
forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp [(Symbol, RTypeV Symbol c tv ())]
xs (UReft Reft -> RTypeV Symbol c tv (UReft Reft)
forall v c tv r. r -> RTypeV v 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, RTypeV Symbol c tv ())]
xs RTypeV Symbol c tv (UReft Reft)
t) = ([(Symbol, RTypeV Symbol c tv ())]
-> RTypeV Symbol c tv (UReft Reft)
-> Ref (RTypeV Symbol c tv ()) (RTypeV Symbol c tv (UReft Reft))
forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp [(Symbol, RTypeV Symbol c tv ())]
xs RTypeV Symbol c tv (UReft Reft)
t1, [(Symbol, RTypeV Symbol c tv ())]
-> RTypeV Symbol c tv (UReft Reft)
-> Ref (RTypeV Symbol c tv ()) (RTypeV Symbol c tv (UReft Reft))
forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp [(Symbol, RTypeV Symbol c tv ())]
xs RTypeV Symbol c tv (UReft Reft)
t2)
  where
        (RTypeV Symbol c tv (UReft Reft)
t1, RTypeV Symbol c tv (UReft Reft)
t2) = Symbol
-> RTypeV Symbol c tv (UReft Reft)
-> (RTypeV Symbol c tv (UReft Reft),
    RTypeV Symbol 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 RTypeV Symbol 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 PredicateV Symbol
p) = (Reft -> PredicateV Symbol -> UReft Reft
forall v r. r -> PredicateV v -> UReftV v r
MkUReft Reft
r1 PredicateV Symbol
p1, Reft -> PredicateV Symbol -> UReft Reft
forall v r. r -> PredicateV v -> UReftV v r
MkUReft Reft
r2 PredicateV Symbol
p2)
        where
                (Reft
r1, Reft
r2) = Symbol -> Reft -> (Reft, Reft)
splitReft Symbol
f Reft
r
                (PredicateV Symbol
p1, PredicateV Symbol
p2) = Symbol
-> PredicateV Symbol -> (PredicateV Symbol, PredicateV Symbol)
splitPred Symbol
f PredicateV Symbol
p

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

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


splitPred :: Symbol -> Predicate -> (Predicate, Predicate)
splitPred :: Symbol
-> PredicateV Symbol -> (PredicateV Symbol, PredicateV Symbol)
splitPred Symbol
f (Pr [UsedPVarV Symbol]
ps) = ([UsedPVarV Symbol] -> PredicateV Symbol
forall v. [UsedPVarV v] -> PredicateV v
Pr [UsedPVarV Symbol]
ps1, [UsedPVarV Symbol] -> PredicateV Symbol
forall v. [UsedPVarV v] -> PredicateV v
Pr [UsedPVarV Symbol]
ps2)
  where
    ([UsedPVarV Symbol]
ps1, [UsedPVarV Symbol]
ps2) = (UsedPVarV Symbol -> Bool)
-> [UsedPVarV Symbol] -> ([UsedPVarV Symbol], [UsedPVarV Symbol])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition UsedPVarV Symbol -> Bool
forall {v} {a}. Subable (ExprV v) => PVarV v a -> Bool
g [UsedPVarV Symbol]
ps
    g :: PVarV v a -> Bool
g PVarV v a
p = (ExprV v -> Bool) -> [ExprV v] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Symbol -> ExprV v -> Bool
forall a. IsFree a => Symbol -> a -> Bool
isFree Symbol
f) ((a, Symbol, ExprV v) -> ExprV v
forall a b c. (a, b, c) -> c
thd3 ((a, Symbol, ExprV v) -> ExprV v)
-> [(a, Symbol, ExprV v)] -> [ExprV v]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PVarV v a -> [(a, Symbol, ExprV v)]
forall v t. PVarV v t -> [(t, Symbol, ExprV v)]
pargs PVarV v 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 a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` x -> [Symbol]
forall a. Subable a => a -> [Symbol]
syms x
p