{-# 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 -> RTypeBV Symbol Symbol c tv (UReft Reft)
forall b v c tv r. tv -> r -> RTypeBV b v c tv r
RVar tv
a UReft Reft
r1, tv -> UReft Reft -> RTypeBV Symbol Symbol c tv (UReft Reft)
forall b v c tv r. tv -> r -> RTypeBV b 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 RTypeBV Symbol Symbol c tv (UReft Reft)
tx RTypeBV Symbol Symbol c tv (UReft Reft)
t UReft Reft
r) = (Symbol
-> RFInfo
-> RTypeBV Symbol Symbol c tv (UReft Reft)
-> RTypeBV Symbol Symbol c tv (UReft Reft)
-> UReft Reft
-> RTypeBV Symbol Symbol c tv (UReft Reft)
forall b v c tv r.
b
-> RFInfo
-> RTypeBV b v c tv r
-> RTypeBV b v c tv r
-> r
-> RTypeBV b v c tv r
RFun Symbol
x RFInfo
i RTypeBV Symbol Symbol c tv (UReft Reft)
tx1 RTypeBV Symbol Symbol c tv (UReft Reft)
t1 UReft Reft
r1, Symbol
-> RFInfo
-> RTypeBV Symbol Symbol c tv (UReft Reft)
-> RTypeBV Symbol Symbol c tv (UReft Reft)
-> UReft Reft
-> RTypeBV Symbol Symbol c tv (UReft Reft)
forall b v c tv r.
b
-> RFInfo
-> RTypeBV b v c tv r
-> RTypeBV b v c tv r
-> r
-> RTypeBV b v c tv r
RFun Symbol
x RFInfo
i RTypeBV Symbol Symbol c tv (UReft Reft)
tx2 RTypeBV Symbol Symbol c tv (UReft Reft)
t2 UReft Reft
r2)
  where
        (RTypeBV Symbol Symbol c tv (UReft Reft)
tx1, RTypeBV Symbol Symbol c tv (UReft Reft)
tx2) = Symbol
-> RTypeBV Symbol Symbol c tv (UReft Reft)
-> (RTypeBV Symbol Symbol c tv (UReft Reft),
    RTypeBV Symbol 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 RTypeBV Symbol Symbol c tv (UReft Reft)
tx
        (RTypeBV Symbol Symbol c tv (UReft Reft)
t1,  RTypeBV Symbol Symbol c tv (UReft Reft)
t2)  = Symbol
-> RTypeBV Symbol Symbol c tv (UReft Reft)
-> (RTypeBV Symbol Symbol c tv (UReft Reft),
    RTypeBV Symbol 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 RTypeBV Symbol 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 RTVUBV Symbol Symbol c tv
v RTypeBV Symbol Symbol c tv (UReft Reft)
t UReft Reft
r) = (RTVUBV Symbol Symbol c tv
-> RTypeBV Symbol Symbol c tv (UReft Reft)
-> UReft Reft
-> RTypeBV Symbol Symbol c tv (UReft Reft)
forall b v c tv r.
RTVUBV b v c tv -> RTypeBV b v c tv r -> r -> RTypeBV b v c tv r
RAllT RTVUBV Symbol Symbol c tv
v RTypeBV Symbol Symbol c tv (UReft Reft)
t1 UReft Reft
r1, RTVUBV Symbol Symbol c tv
-> RTypeBV Symbol Symbol c tv (UReft Reft)
-> UReft Reft
-> RTypeBV Symbol Symbol c tv (UReft Reft)
forall b v c tv r.
RTVUBV b v c tv -> RTypeBV b v c tv r -> r -> RTypeBV b v c tv r
RAllT RTVUBV Symbol Symbol c tv
v RTypeBV Symbol Symbol c tv (UReft Reft)
t2 UReft Reft
r2)
  where
        (RTypeBV Symbol Symbol c tv (UReft Reft)
t1, RTypeBV Symbol Symbol c tv (UReft Reft)
t2) = Symbol
-> RTypeBV Symbol Symbol c tv (UReft Reft)
-> (RTypeBV Symbol Symbol c tv (UReft Reft),
    RTypeBV Symbol 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 RTypeBV Symbol 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 PVUBV Symbol Symbol c tv
p RTypeBV Symbol Symbol c tv (UReft Reft)
t) = (PVUBV Symbol Symbol c tv
-> RTypeBV Symbol Symbol c tv (UReft Reft)
-> RTypeBV Symbol Symbol c tv (UReft Reft)
forall b v c tv r.
PVUBV b v c tv -> RTypeBV b v c tv r -> RTypeBV b v c tv r
RAllP PVUBV Symbol Symbol c tv
p RTypeBV Symbol Symbol c tv (UReft Reft)
t1, PVUBV Symbol Symbol c tv
-> RTypeBV Symbol Symbol c tv (UReft Reft)
-> RTypeBV Symbol Symbol c tv (UReft Reft)
forall b v c tv r.
PVUBV b v c tv -> RTypeBV b v c tv r -> RTypeBV b v c tv r
RAllP PVUBV Symbol Symbol c tv
p RTypeBV Symbol Symbol c tv (UReft Reft)
t2)
  where
        (RTypeBV Symbol Symbol c tv (UReft Reft)
t1, RTypeBV Symbol Symbol c tv (UReft Reft)
t2) = Symbol
-> RTypeBV Symbol Symbol c tv (UReft Reft)
-> (RTypeBV Symbol Symbol c tv (UReft Reft),
    RTypeBV Symbol 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 RTypeBV Symbol Symbol c tv (UReft Reft)
t
splitRType Symbol
f (RApp c
c [RTypeBV Symbol Symbol c tv (UReft Reft)]
ts [RTPropBV Symbol Symbol c tv (UReft Reft)]
rs UReft Reft
r) = (c
-> [RTypeBV Symbol Symbol c tv (UReft Reft)]
-> [RTPropBV Symbol Symbol c tv (UReft Reft)]
-> UReft Reft
-> RTypeBV Symbol Symbol c tv (UReft Reft)
forall b v c tv r.
c
-> [RTypeBV b v c tv r]
-> [RTPropBV b v c tv r]
-> r
-> RTypeBV b v c tv r
RApp c
c [RTypeBV Symbol Symbol c tv (UReft Reft)]
ts1 [RTPropBV Symbol Symbol c tv (UReft Reft)]
rs1 UReft Reft
r1, c
-> [RTypeBV Symbol Symbol c tv (UReft Reft)]
-> [RTPropBV Symbol Symbol c tv (UReft Reft)]
-> UReft Reft
-> RTypeBV Symbol Symbol c tv (UReft Reft)
forall b v c tv r.
c
-> [RTypeBV b v c tv r]
-> [RTPropBV b v c tv r]
-> r
-> RTypeBV b v c tv r
RApp c
c [RTypeBV Symbol Symbol c tv (UReft Reft)]
ts2 [RTPropBV Symbol Symbol c tv (UReft Reft)]
rs2 UReft Reft
r2)
  where
        ([RTypeBV Symbol Symbol c tv (UReft Reft)]
ts1, [RTypeBV Symbol Symbol c tv (UReft Reft)]
ts2) = [(RTypeBV Symbol Symbol c tv (UReft Reft),
  RTypeBV Symbol Symbol c tv (UReft Reft))]
-> ([RTypeBV Symbol Symbol c tv (UReft Reft)],
    [RTypeBV Symbol Symbol c tv (UReft Reft)])
forall a b. [(a, b)] -> ([a], [b])
unzip (Symbol
-> RTypeBV Symbol Symbol c tv (UReft Reft)
-> (RTypeBV Symbol Symbol c tv (UReft Reft),
    RTypeBV Symbol 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 (RTypeBV Symbol Symbol c tv (UReft Reft)
 -> (RTypeBV Symbol Symbol c tv (UReft Reft),
     RTypeBV Symbol Symbol c tv (UReft Reft)))
-> [RTypeBV Symbol Symbol c tv (UReft Reft)]
-> [(RTypeBV Symbol Symbol c tv (UReft Reft),
     RTypeBV Symbol Symbol c tv (UReft Reft))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RTypeBV Symbol Symbol c tv (UReft Reft)]
ts)
        ([RTPropBV Symbol Symbol c tv (UReft Reft)]
rs1, [RTPropBV Symbol Symbol c tv (UReft Reft)]
rs2) = [(RTPropBV Symbol Symbol c tv (UReft Reft),
  RTPropBV Symbol Symbol c tv (UReft Reft))]
-> ([RTPropBV Symbol Symbol c tv (UReft Reft)],
    [RTPropBV Symbol Symbol c tv (UReft Reft)])
forall a b. [(a, b)] -> ([a], [b])
unzip (Symbol
-> RTPropBV Symbol Symbol c tv (UReft Reft)
-> (RTPropBV Symbol Symbol c tv (UReft Reft),
    RTPropBV Symbol 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 (RTPropBV Symbol Symbol c tv (UReft Reft)
 -> (RTPropBV Symbol Symbol c tv (UReft Reft),
     RTPropBV Symbol Symbol c tv (UReft Reft)))
-> [RTPropBV Symbol Symbol c tv (UReft Reft)]
-> [(RTPropBV Symbol Symbol c tv (UReft Reft),
     RTPropBV Symbol Symbol c tv (UReft Reft))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RTPropBV Symbol 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 RTypeBV Symbol Symbol c tv (UReft Reft)
tx RTypeBV Symbol Symbol c tv (UReft Reft)
t) = (Symbol
-> RTypeBV Symbol Symbol c tv (UReft Reft)
-> RTypeBV Symbol Symbol c tv (UReft Reft)
-> RTypeBV Symbol Symbol c tv (UReft Reft)
forall b v c tv r.
b -> RTypeBV b v c tv r -> RTypeBV b v c tv r -> RTypeBV b v c tv r
RAllE Symbol
x RTypeBV Symbol Symbol c tv (UReft Reft)
tx1 RTypeBV Symbol Symbol c tv (UReft Reft)
t1, Symbol
-> RTypeBV Symbol Symbol c tv (UReft Reft)
-> RTypeBV Symbol Symbol c tv (UReft Reft)
-> RTypeBV Symbol Symbol c tv (UReft Reft)
forall b v c tv r.
b -> RTypeBV b v c tv r -> RTypeBV b v c tv r -> RTypeBV b v c tv r
RAllE Symbol
x RTypeBV Symbol Symbol c tv (UReft Reft)
tx2 RTypeBV Symbol Symbol c tv (UReft Reft)
t2)
  where
        (RTypeBV Symbol Symbol c tv (UReft Reft)
tx1, RTypeBV Symbol Symbol c tv (UReft Reft)
tx2) = Symbol
-> RTypeBV Symbol Symbol c tv (UReft Reft)
-> (RTypeBV Symbol Symbol c tv (UReft Reft),
    RTypeBV Symbol 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 RTypeBV Symbol Symbol c tv (UReft Reft)
tx
        (RTypeBV Symbol Symbol c tv (UReft Reft)
t1, RTypeBV Symbol Symbol c tv (UReft Reft)
t2)   = Symbol
-> RTypeBV Symbol Symbol c tv (UReft Reft)
-> (RTypeBV Symbol Symbol c tv (UReft Reft),
    RTypeBV Symbol 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 RTypeBV Symbol Symbol c tv (UReft Reft)
t
splitRType Symbol
f (REx Symbol
x RTypeBV Symbol Symbol c tv (UReft Reft)
tx RTypeBV Symbol Symbol c tv (UReft Reft)
t) = (Symbol
-> RTypeBV Symbol Symbol c tv (UReft Reft)
-> RTypeBV Symbol Symbol c tv (UReft Reft)
-> RTypeBV Symbol Symbol c tv (UReft Reft)
forall b v c tv r.
b -> RTypeBV b v c tv r -> RTypeBV b v c tv r -> RTypeBV b v c tv r
REx Symbol
x RTypeBV Symbol Symbol c tv (UReft Reft)
tx1 RTypeBV Symbol Symbol c tv (UReft Reft)
t1, Symbol
-> RTypeBV Symbol Symbol c tv (UReft Reft)
-> RTypeBV Symbol Symbol c tv (UReft Reft)
-> RTypeBV Symbol Symbol c tv (UReft Reft)
forall b v c tv r.
b -> RTypeBV b v c tv r -> RTypeBV b v c tv r -> RTypeBV b v c tv r
REx Symbol
x RTypeBV Symbol Symbol c tv (UReft Reft)
tx2 RTypeBV Symbol Symbol c tv (UReft Reft)
t2)
  where
        (RTypeBV Symbol Symbol c tv (UReft Reft)
tx1, RTypeBV Symbol Symbol c tv (UReft Reft)
tx2) = Symbol
-> RTypeBV Symbol Symbol c tv (UReft Reft)
-> (RTypeBV Symbol Symbol c tv (UReft Reft),
    RTypeBV Symbol 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 RTypeBV Symbol Symbol c tv (UReft Reft)
tx
        (RTypeBV Symbol Symbol c tv (UReft Reft)
t1, RTypeBV Symbol Symbol c tv (UReft Reft)
t2)   = Symbol
-> RTypeBV Symbol Symbol c tv (UReft Reft)
-> (RTypeBV Symbol Symbol c tv (UReft Reft),
    RTypeBV Symbol 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 RTypeBV Symbol Symbol c tv (UReft Reft)
t
splitRType Symbol
_ (RExprArg Located (ExprBV Symbol Symbol)
e) = (Located (ExprBV Symbol Symbol)
-> RTypeBV Symbol Symbol c tv (UReft Reft)
forall b v c tv r. Located (ExprBV b v) -> RTypeBV b v c tv r
RExprArg Located (ExprBV Symbol Symbol)
e, Located (ExprBV Symbol Symbol)
-> RTypeBV Symbol Symbol c tv (UReft Reft)
forall b v c tv r. Located (ExprBV b v) -> RTypeBV b v c tv r
RExprArg Located (ExprBV Symbol Symbol)
e)
splitRType Symbol
f (RAppTy RTypeBV Symbol Symbol c tv (UReft Reft)
tx RTypeBV Symbol Symbol c tv (UReft Reft)
t UReft Reft
r) = (RTypeBV Symbol Symbol c tv (UReft Reft)
-> RTypeBV Symbol Symbol c tv (UReft Reft)
-> UReft Reft
-> RTypeBV Symbol Symbol c tv (UReft Reft)
forall b v c tv r.
RTypeBV b v c tv r -> RTypeBV b v c tv r -> r -> RTypeBV b v c tv r
RAppTy RTypeBV Symbol Symbol c tv (UReft Reft)
tx1 RTypeBV Symbol Symbol c tv (UReft Reft)
t1 UReft Reft
r1, RTypeBV Symbol Symbol c tv (UReft Reft)
-> RTypeBV Symbol Symbol c tv (UReft Reft)
-> UReft Reft
-> RTypeBV Symbol Symbol c tv (UReft Reft)
forall b v c tv r.
RTypeBV b v c tv r -> RTypeBV b v c tv r -> r -> RTypeBV b v c tv r
RAppTy RTypeBV Symbol Symbol c tv (UReft Reft)
tx2 RTypeBV Symbol Symbol c tv (UReft Reft)
t2 UReft Reft
r2)
  where
        (RTypeBV Symbol Symbol c tv (UReft Reft)
tx1, RTypeBV Symbol Symbol c tv (UReft Reft)
tx2) = Symbol
-> RTypeBV Symbol Symbol c tv (UReft Reft)
-> (RTypeBV Symbol Symbol c tv (UReft Reft),
    RTypeBV Symbol 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 RTypeBV Symbol Symbol c tv (UReft Reft)
tx
        (RTypeBV Symbol Symbol c tv (UReft Reft)
t1,  RTypeBV Symbol Symbol c tv (UReft Reft)
t2)  = Symbol
-> RTypeBV Symbol Symbol c tv (UReft Reft)
-> (RTypeBV Symbol Symbol c tv (UReft Reft),
    RTypeBV Symbol 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 RTypeBV Symbol 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, RTypeBV Symbol Symbol c tv (UReft Reft))]
xs UReft Reft
r Oblig
o RTypeBV Symbol Symbol c tv (UReft Reft)
rt) = ([(Symbol, RTypeBV Symbol Symbol c tv (UReft Reft))]
-> UReft Reft
-> Oblig
-> RTypeBV Symbol Symbol c tv (UReft Reft)
-> RTypeBV Symbol Symbol c tv (UReft Reft)
forall b v c tv r.
[(b, RTypeBV b v c tv r)]
-> r -> Oblig -> RTypeBV b v c tv r -> RTypeBV b v c tv r
RRTy [(Symbol, RTypeBV Symbol Symbol c tv (UReft Reft))]
xs1 UReft Reft
r1 Oblig
o RTypeBV Symbol Symbol c tv (UReft Reft)
rt1, [(Symbol, RTypeBV Symbol Symbol c tv (UReft Reft))]
-> UReft Reft
-> Oblig
-> RTypeBV Symbol Symbol c tv (UReft Reft)
-> RTypeBV Symbol Symbol c tv (UReft Reft)
forall b v c tv r.
[(b, RTypeBV b v c tv r)]
-> r -> Oblig -> RTypeBV b v c tv r -> RTypeBV b v c tv r
RRTy [(Symbol, RTypeBV Symbol Symbol c tv (UReft Reft))]
xs2 UReft Reft
r2 Oblig
o RTypeBV Symbol Symbol c tv (UReft Reft)
rt2)
  where
        ([(Symbol, RTypeBV Symbol Symbol c tv (UReft Reft))]
xs1, [(Symbol, RTypeBV Symbol Symbol c tv (UReft Reft))]
xs2) = [((Symbol, RTypeBV Symbol Symbol c tv (UReft Reft)),
  (Symbol, RTypeBV Symbol Symbol c tv (UReft Reft)))]
-> ([(Symbol, RTypeBV Symbol Symbol c tv (UReft Reft))],
    [(Symbol, RTypeBV Symbol Symbol c tv (UReft Reft))])
forall a b. [(a, b)] -> ([a], [b])
unzip ((Symbol, RTypeBV Symbol Symbol c tv (UReft Reft))
-> ((Symbol, RTypeBV Symbol Symbol c tv (UReft Reft)),
    (Symbol, RTypeBV Symbol Symbol c tv (UReft Reft)))
forall {a} {c} {tv}.
(a, RTypeBV Symbol Symbol c tv (UReft Reft))
-> ((a, RTypeBV Symbol Symbol c tv (UReft Reft)),
    (a, RTypeBV Symbol Symbol c tv (UReft Reft)))
go ((Symbol, RTypeBV Symbol Symbol c tv (UReft Reft))
 -> ((Symbol, RTypeBV Symbol Symbol c tv (UReft Reft)),
     (Symbol, RTypeBV Symbol Symbol c tv (UReft Reft))))
-> [(Symbol, RTypeBV Symbol Symbol c tv (UReft Reft))]
-> [((Symbol, RTypeBV Symbol Symbol c tv (UReft Reft)),
     (Symbol, RTypeBV Symbol Symbol c tv (UReft Reft)))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, RTypeBV Symbol 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
        (RTypeBV Symbol Symbol c tv (UReft Reft)
rt1, RTypeBV Symbol Symbol c tv (UReft Reft)
rt2) = Symbol
-> RTypeBV Symbol Symbol c tv (UReft Reft)
-> (RTypeBV Symbol Symbol c tv (UReft Reft),
    RTypeBV Symbol 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 RTypeBV Symbol Symbol c tv (UReft Reft)
rt

        go :: (a, RTypeBV Symbol Symbol c tv (UReft Reft))
-> ((a, RTypeBV Symbol Symbol c tv (UReft Reft)),
    (a, RTypeBV Symbol Symbol c tv (UReft Reft)))
go (a
x, RTypeBV Symbol Symbol c tv (UReft Reft)
t) = let (RTypeBV Symbol Symbol c tv (UReft Reft)
t1, RTypeBV Symbol Symbol c tv (UReft Reft)
t2) = Symbol
-> RTypeBV Symbol Symbol c tv (UReft Reft)
-> (RTypeBV Symbol Symbol c tv (UReft Reft),
    RTypeBV Symbol 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 RTypeBV Symbol Symbol c tv (UReft Reft)
t in ((a
x,RTypeBV Symbol Symbol c tv (UReft Reft)
t1), (a
x, RTypeBV Symbol Symbol c tv (UReft Reft)
t2))
splitRType Symbol
f (RHole UReft Reft
r) = (UReft Reft -> RTypeBV Symbol Symbol c tv (UReft Reft)
forall b v c tv r. r -> RTypeBV b v c tv r
RHole UReft Reft
r1, UReft Reft -> RTypeBV Symbol Symbol c tv (UReft Reft)
forall b v c tv r. r -> RTypeBV b 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, RTypeBV Symbol Symbol c tv (NoReftB Symbol))]
xs (RHole UReft Reft
r)) = ([(Symbol, RTypeBV Symbol Symbol c tv (NoReftB Symbol))]
-> RTypeBV Symbol Symbol c tv (UReft Reft)
-> RefB
     Symbol
     (RTypeBV Symbol Symbol c tv (NoReftB Symbol))
     (RTypeBV Symbol Symbol c tv (UReft Reft))
forall b τ t. [(b, τ)] -> t -> RefB b τ t
RProp [(Symbol, RTypeBV Symbol Symbol c tv (NoReftB Symbol))]
xs (UReft Reft -> RTypeBV Symbol Symbol c tv (UReft Reft)
forall b v c tv r. r -> RTypeBV b v c tv r
RHole UReft Reft
r1), [(Symbol, RTypeBV Symbol Symbol c tv (NoReftB Symbol))]
-> RTypeBV Symbol Symbol c tv (UReft Reft)
-> RefB
     Symbol
     (RTypeBV Symbol Symbol c tv (NoReftB Symbol))
     (RTypeBV Symbol Symbol c tv (UReft Reft))
forall b τ t. [(b, τ)] -> t -> RefB b τ t
RProp [(Symbol, RTypeBV Symbol Symbol c tv (NoReftB Symbol))]
xs (UReft Reft -> RTypeBV Symbol Symbol c tv (UReft Reft)
forall b v c tv r. r -> RTypeBV b 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, RTypeBV Symbol Symbol c tv (NoReftB Symbol))]
xs RTypeBV Symbol Symbol c tv (UReft Reft)
t) = ([(Symbol, RTypeBV Symbol Symbol c tv (NoReftB Symbol))]
-> RTypeBV Symbol Symbol c tv (UReft Reft)
-> RefB
     Symbol
     (RTypeBV Symbol Symbol c tv (NoReftB Symbol))
     (RTypeBV Symbol Symbol c tv (UReft Reft))
forall b τ t. [(b, τ)] -> t -> RefB b τ t
RProp [(Symbol, RTypeBV Symbol Symbol c tv (NoReftB Symbol))]
xs RTypeBV Symbol Symbol c tv (UReft Reft)
t1, [(Symbol, RTypeBV Symbol Symbol c tv (NoReftB Symbol))]
-> RTypeBV Symbol Symbol c tv (UReft Reft)
-> RefB
     Symbol
     (RTypeBV Symbol Symbol c tv (NoReftB Symbol))
     (RTypeBV Symbol Symbol c tv (UReft Reft))
forall b τ t. [(b, τ)] -> t -> RefB b τ t
RProp [(Symbol, RTypeBV Symbol Symbol c tv (NoReftB Symbol))]
xs RTypeBV Symbol Symbol c tv (UReft Reft)
t2)
  where
        (RTypeBV Symbol Symbol c tv (UReft Reft)
t1, RTypeBV Symbol Symbol c tv (UReft Reft)
t2) = Symbol
-> RTypeBV Symbol Symbol c tv (UReft Reft)
-> (RTypeBV Symbol Symbol c tv (UReft Reft),
    RTypeBV Symbol 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 RTypeBV Symbol 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 PredicateBV Symbol Symbol
p) = (Reft -> PredicateBV Symbol Symbol -> UReft Reft
forall b v r. r -> PredicateBV b v -> UReftBV b v r
MkUReft Reft
r1 PredicateBV Symbol Symbol
p1, Reft -> PredicateBV Symbol Symbol -> UReft Reft
forall b v r. r -> PredicateBV b v -> UReftBV b v r
MkUReft Reft
r2 PredicateBV Symbol Symbol
p2)
        where
                (Reft
r1, Reft
r2) = Symbol -> Reft -> (Reft, Reft)
splitReft Symbol
f Reft
r
                (PredicateBV Symbol Symbol
p1, PredicateBV Symbol Symbol
p2) = Symbol
-> PredicateBV Symbol Symbol
-> (PredicateBV Symbol Symbol, PredicateBV Symbol Symbol)
splitPred Symbol
f PredicateBV Symbol Symbol
p

splitReft :: Symbol -> Reft -> (Reft, Reft)
splitReft :: Symbol -> Reft -> (Reft, Reft)
splitReft Symbol
f (Reft (Symbol
v, ExprBV Symbol Symbol
xs)) = ((Symbol, ExprBV Symbol Symbol) -> Reft
forall b v. (b, ExprBV b v) -> ReftBV b v
Reft (Symbol
v, ListNE (ExprBV Symbol Symbol) -> ExprBV Symbol Symbol
forall b v.
(Ord b, Hashable b, Ord v) =>
ListNE (ExprBV b v) -> ExprBV b v
pAnd ListNE (ExprBV Symbol Symbol)
xs1), (Symbol, ExprBV Symbol Symbol) -> Reft
forall b v. (b, ExprBV b v) -> ReftBV b v
Reft (Symbol
v, ListNE (ExprBV Symbol Symbol) -> ExprBV Symbol Symbol
forall b v.
(Ord b, Hashable b, Ord v) =>
ListNE (ExprBV b v) -> ExprBV b v
pAnd ListNE (ExprBV Symbol Symbol)
xs2))
  where
    (ListNE (ExprBV Symbol Symbol)
xs1, ListNE (ExprBV Symbol Symbol)
xs2)       = (ExprBV Symbol Symbol -> Bool)
-> ListNE (ExprBV Symbol Symbol)
-> (ListNE (ExprBV Symbol Symbol), ListNE (ExprBV Symbol Symbol))
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (Variable (ExprBV Symbol Symbol) -> ExprBV Symbol Symbol -> Bool
forall a. IsFree a => Variable a -> a -> Bool
isFree Symbol
Variable (ExprBV Symbol Symbol)
f) (ExprBV Symbol Symbol -> ListNE (ExprBV Symbol Symbol)
forall {b} {v}. ExprBV b v -> [ExprBV b v]
unPAnd ExprBV Symbol Symbol
xs)

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


splitPred :: Symbol -> Predicate -> (Predicate, Predicate)
splitPred :: Symbol
-> PredicateBV Symbol Symbol
-> (PredicateBV Symbol Symbol, PredicateBV Symbol Symbol)
splitPred Symbol
f (Pr [UsedPVarBV Symbol Symbol]
ps) = ([UsedPVarBV Symbol Symbol] -> PredicateBV Symbol Symbol
forall b v. [UsedPVarBV b v] -> PredicateBV b v
Pr [UsedPVarBV Symbol Symbol]
ps1, [UsedPVarBV Symbol Symbol] -> PredicateBV Symbol Symbol
forall b v. [UsedPVarBV b v] -> PredicateBV b v
Pr [UsedPVarBV Symbol Symbol]
ps2)
  where
    ([UsedPVarBV Symbol Symbol]
ps1, [UsedPVarBV Symbol Symbol]
ps2) = (UsedPVarBV Symbol Symbol -> Bool)
-> [UsedPVarBV Symbol Symbol]
-> ([UsedPVarBV Symbol Symbol], [UsedPVarBV Symbol Symbol])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition UsedPVarBV Symbol Symbol -> Bool
forall {b} {v} {a}.
(Variable (ExprBV b v) ~ Symbol, Subable (ExprBV b v)) =>
PVarBV b v a -> Bool
g [UsedPVarBV Symbol Symbol]
ps
    g :: PVarBV b v a -> Bool
g PVarBV b v a
p = (ExprBV b v -> Bool) -> [ExprBV b v] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Variable (ExprBV b v) -> ExprBV b v -> Bool
forall a. IsFree a => Variable a -> a -> Bool
isFree Symbol
Variable (ExprBV b v)
f) ((a, b, ExprBV b v) -> ExprBV b v
forall a b c. (a, b, c) -> c
thd3 ((a, b, ExprBV b v) -> ExprBV b v)
-> [(a, b, ExprBV b v)] -> [ExprBV b v]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PVarBV b v a -> [(a, b, ExprBV b v)]
forall b v t. PVarBV b v t -> [(t, b, ExprBV b v)]
pargs PVarBV b v a
p)


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

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