{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}

module DataFrame.Internal.Simplify (
    simplify,
    simplifyPredicatePair,

    -- * Path-condition entailment (for fitted-tree pruning)
    PredFact,
    factTrue,
    factFalse,
    entails,
) where

import Control.Monad (guard)
import Data.Maybe (fromMaybe)
import Data.Type.Equality (testEquality, (:~:) (Refl))
import Type.Reflection (eqTypeRep, typeRep, (:~~:) (HRefl), pattern App)

import DataFrame.Internal.Column (Columnable)
import DataFrame.Internal.Expression (
    BinaryOp,
    Expr (..),
    UnaryOp (unaryName),
    eqExpr,
    normalize,
 )
import DataFrame.Operators (
    NullAnd,
    NullEq,
    NullGeq,
    NullGt,
    NullLeq,
    NullLt,
    NullNeq,
    NullOr,
    (.==.),
 )

simplify :: forall a. (Columnable a) => Expr a -> Expr a
simplify :: forall a. Columnable a => Expr a -> Expr a
simplify Expr a
e
    | forall a. Columnable a => Bool
isBoolish @a = Int -> Expr a -> Expr a
forall {a} {t}.
(When (Unboxable a) (Unbox a), When (IntegralTypes a) (Integral a),
 When (FloatingTypes a) (Real a, Fractional a), Num t, Typeable a,
 Show a, Eq t, Eq a, ColumnifyRep (KindOf a) a,
 SBoolI (Unboxable a), SBoolI (Numeric a), SBoolI (IntegralTypes a),
 SBoolI (FloatingTypes a)) =>
t -> Expr a -> Expr a
fixpoint (Int
10 :: Int) Expr a
e
    | Bool
otherwise = Expr a
e
  where
    fixpoint :: t -> Expr a -> Expr a
fixpoint t
0 Expr a
x = Expr a
x
    fixpoint t
n Expr a
x = let x' :: Expr a
x' = Expr a -> Expr a
forall a. Columnable a => Expr a -> Expr a
simplifyB Expr a
x in if Expr a -> Expr a -> Bool
forall a. Columnable a => Expr a -> Expr a -> Bool
eqExpr Expr a
x Expr a
x' then Expr a
x else t -> Expr a -> Expr a
fixpoint (t
n t -> t -> t
forall a. Num a => a -> a -> a
- t
1) Expr a
x'

isBoolish :: forall a. (Columnable a) => Bool
isBoolish :: forall a. Columnable a => Bool
isBoolish =
    case ( TypeRep a -> TypeRep Bool -> Maybe (a :~: Bool)
forall a b. TypeRep a -> TypeRep b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @a) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @Bool)
         , TypeRep a -> TypeRep (Maybe Bool) -> Maybe (a :~: Maybe Bool)
forall a b. TypeRep a -> TypeRep b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @a) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @(Maybe Bool))
         ) of
        (Just a :~: Bool
Refl, Maybe (a :~: Maybe Bool)
_) -> Bool
True
        (Maybe (a :~: Bool)
_, Just a :~: Maybe Bool
Refl) -> Bool
True
        (Maybe (a :~: Bool), Maybe (a :~: Maybe Bool))
_ -> Bool
False

data Conn = ConnAnd | ConnOr

connOf :: forall op c b r. (BinaryOp op) => op c b r -> Maybe Conn
connOf :: forall (op :: * -> * -> * -> *) c b r.
BinaryOp op =>
op c b r -> Maybe Conn
connOf op c b r
_
    | Just op :~~: NullAnd
HRefl <- TypeRep op -> TypeRep NullAnd -> Maybe (op :~~: NullAnd)
forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
eqTypeRep (forall {k} (a :: k). Typeable a => TypeRep a
forall (a :: * -> * -> * -> *). Typeable a => TypeRep a
typeRep @op) (forall {k} (a :: k). Typeable a => TypeRep a
forall (a :: * -> * -> * -> *). Typeable a => TypeRep a
typeRep @NullAnd) = Conn -> Maybe Conn
forall a. a -> Maybe a
Just Conn
ConnAnd
    | Just op :~~: NullOr
HRefl <- TypeRep op -> TypeRep NullOr -> Maybe (op :~~: NullOr)
forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
eqTypeRep (forall {k} (a :: k). Typeable a => TypeRep a
forall (a :: * -> * -> * -> *). Typeable a => TypeRep a
typeRep @op) (forall {k} (a :: k). Typeable a => TypeRep a
forall (a :: * -> * -> * -> *). Typeable a => TypeRep a
typeRep @NullOr) = Conn -> Maybe Conn
forall a. a -> Maybe a
Just Conn
ConnOr
    | Bool
otherwise = Maybe Conn
forall a. Maybe a
Nothing

simplifyB :: forall a. (Columnable a) => Expr a -> Expr a
simplifyB :: forall a. Columnable a => Expr a -> Expr a
simplifyB Expr a
expr = case Expr a
expr of
    Binary (op c b a
op :: op c b a) Expr c
l Expr b
r
        | Just Conn
conn <- op c b a -> Maybe Conn
forall (op :: * -> * -> * -> *) c b r.
BinaryOp op =>
op c b r -> Maybe Conn
connOf op c b a
op
        , Just c :~: a
Refl <- TypeRep c -> TypeRep a -> Maybe (c :~: a)
forall a b. TypeRep a -> TypeRep b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @c) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @a)
        , Just b :~: a
Refl <- TypeRep b -> TypeRep a -> Maybe (b :~: a)
forall a b. TypeRep a -> TypeRep b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @b) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @a) ->
            let l' :: Expr c
l' = Expr c -> Expr c
forall a. Columnable a => Expr a -> Expr a
simplifyB Expr c
l; r' :: Expr b
r' = Expr b -> Expr b
forall a. Columnable a => Expr a -> Expr a
simplifyB Expr b
r
             in Expr a -> Maybe (Expr a) -> Expr a
forall a. a -> Maybe a -> a
fromMaybe (op c b a -> Expr c -> Expr b -> Expr a
forall (op :: * -> * -> * -> *) c b a.
(BinaryOp op, Columnable c, Columnable b, Columnable a) =>
op c b a -> Expr c -> Expr b -> Expr a
Binary op c b a
op Expr c
l' Expr b
r') (Conn -> Expr a -> Expr a -> Maybe (Expr a)
forall a.
Columnable a =>
Conn -> Expr a -> Expr a -> Maybe (Expr a)
combine Conn
conn Expr a
Expr c
l' Expr a
Expr b
r')
        | Bool
otherwise -> Expr a
expr
    Unary (op b a
op :: op b a) Expr b
inner
        | Just a :~: Bool
Refl <- TypeRep a -> TypeRep Bool -> Maybe (a :~: Bool)
forall a b. TypeRep a -> TypeRep b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @a) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @Bool)
        , Just b :~: Bool
Refl <- TypeRep b -> TypeRep Bool -> Maybe (b :~: Bool)
forall a b. TypeRep a -> TypeRep b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @b) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @Bool)
        , op b a -> Text
forall a b. op a b -> Text
forall (op :: * -> * -> *) a b. UnaryOp op => op a b -> Text
unaryName op b a
op Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
"not" ->
            op Bool Bool -> Expr Bool -> Expr Bool
forall (op :: * -> * -> *).
UnaryOp op =>
op Bool Bool -> Expr Bool -> Expr Bool
simplifyNot op b a
op Bool Bool
op (Expr Bool -> Expr Bool
forall a. Columnable a => Expr a -> Expr a
simplifyB Expr b
Expr Bool
inner)
        | Bool
otherwise -> Expr a
expr
    If Expr Bool
c Expr a
t Expr a
f ->
        let c' :: Expr Bool
c' = Expr Bool -> Expr Bool
forall a. Columnable a => Expr a -> Expr a
simplify Expr Bool
c
            t' :: Expr a
t' = Expr a -> Expr a
forall a. Columnable a => Expr a -> Expr a
simplifyB Expr a
t
            f' :: Expr a
f' = Expr a -> Expr a
forall a. Columnable a => Expr a -> Expr a
simplifyB Expr a
f
         in case Expr Bool -> Maybe Bool
forall a. Columnable a => Expr a -> Maybe Bool
asBoolLit Expr Bool
c' of
                Just Bool
True -> Expr a
t'
                Just Bool
False -> Expr a
f'
                Maybe Bool
Nothing
                    | Expr a -> Expr a -> Bool
forall a. Columnable a => Expr a -> Expr a -> Bool
eqExpr Expr a
t' Expr a
f' -> Expr a
t'
                    | Just a :~: Bool
Refl <- TypeRep a -> TypeRep Bool -> Maybe (a :~: Bool)
forall a b. TypeRep a -> TypeRep b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @a) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @Bool)
                    , Expr a -> Maybe Bool
forall a. Columnable a => Expr a -> Maybe Bool
asBoolLit Expr a
t' Maybe Bool -> Maybe Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True
                    , Expr a -> Maybe Bool
forall a. Columnable a => Expr a -> Maybe Bool
asBoolLit Expr a
f' Maybe Bool -> Maybe Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False ->
                        Expr a
Expr Bool
c'
                    | Bool
otherwise -> Expr Bool -> Expr a -> Expr a -> Expr a
forall a. Columnable a => Expr Bool -> Expr a -> Expr a -> Expr a
If Expr Bool
c' Expr a
t' Expr a
f'
    Expr a
_ -> Expr a
expr

simplifyNot :: (UnaryOp op) => op Bool Bool -> Expr Bool -> Expr Bool
simplifyNot :: forall (op :: * -> * -> *).
UnaryOp op =>
op Bool Bool -> Expr Bool -> Expr Bool
simplifyNot op Bool Bool
op Expr Bool
inner = case Expr Bool -> Maybe Bool
forall a. Columnable a => Expr a -> Maybe Bool
asBoolLit Expr Bool
inner of
    Just Bool
b -> Bool -> Expr Bool
forall a. Columnable a => a -> Expr a
Lit (Bool -> Bool
not Bool
b)
    Maybe Bool
Nothing -> case Expr Bool
inner of
        Unary (op b Bool
op2 :: op2 b2 Bool) Expr b
inner2
            | op b Bool -> Text
forall a b. op a b -> Text
forall (op :: * -> * -> *) a b. UnaryOp op => op a b -> Text
unaryName op b Bool
op2 Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
"not"
            , Just b :~: Bool
Refl <- TypeRep b -> TypeRep Bool -> Maybe (b :~: Bool)
forall a b. TypeRep a -> TypeRep b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @b2) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @Bool) ->
                Expr b
Expr Bool
inner2
        Expr Bool
_ -> op Bool Bool -> Expr Bool -> Expr Bool
forall (op :: * -> * -> *) a b.
(UnaryOp op, Columnable a, Columnable b) =>
op b a -> Expr b -> Expr a
Unary op Bool Bool
op Expr Bool
inner

combine :: (Columnable a) => Conn -> Expr a -> Expr a -> Maybe (Expr a)
combine :: forall a.
Columnable a =>
Conn -> Expr a -> Expr a -> Maybe (Expr a)
combine Conn
ConnAnd = Expr a -> Expr a -> Maybe (Expr a)
forall a. Columnable a => Expr a -> Expr a -> Maybe (Expr a)
combineAnd
combine Conn
ConnOr = Expr a -> Expr a -> Maybe (Expr a)
forall a. Columnable a => Expr a -> Expr a -> Maybe (Expr a)
combineOr

asBoolLit :: forall a. (Columnable a) => Expr a -> Maybe Bool
asBoolLit :: forall a. Columnable a => Expr a -> Maybe Bool
asBoolLit (Lit a
v) =
    case TypeRep a -> TypeRep Bool -> Maybe (a :~: Bool)
forall a b. TypeRep a -> TypeRep b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @a) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @Bool) of
        Just a :~: Bool
Refl -> Bool -> Maybe Bool
forall a. a -> Maybe a
Just a
Bool
v
        Maybe (a :~: Bool)
Nothing -> case TypeRep a -> TypeRep (Maybe Bool) -> Maybe (a :~: Maybe Bool)
forall a b. TypeRep a -> TypeRep b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @a) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @(Maybe Bool)) of
            Just a :~: Maybe Bool
Refl -> a
Maybe Bool
v
            Maybe (a :~: Maybe Bool)
Nothing -> Maybe Bool
forall a. Maybe a
Nothing
asBoolLit Expr a
_ = Maybe Bool
forall a. Maybe a
Nothing

{- | Polymorphic boolean literal: @Lit b@ for @Expr Bool@, @Lit (Just b)@ for
@Expr (Maybe Bool)@.
-}
litBoolish :: forall a. (Columnable a) => Bool -> Maybe (Expr a)
litBoolish :: forall a. Columnable a => Bool -> Maybe (Expr a)
litBoolish Bool
v =
    case TypeRep a -> TypeRep Bool -> Maybe (a :~: Bool)
forall a b. TypeRep a -> TypeRep b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @a) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @Bool) of
        Just a :~: Bool
Refl -> Expr a -> Maybe (Expr a)
forall a. a -> Maybe a
Just (a -> Expr a
forall a. Columnable a => a -> Expr a
Lit a
Bool
v)
        Maybe (a :~: Bool)
Nothing -> case TypeRep a -> TypeRep (Maybe Bool) -> Maybe (a :~: Maybe Bool)
forall a b. TypeRep a -> TypeRep b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @a) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @(Maybe Bool)) of
            Just a :~: Maybe Bool
Refl -> Expr a -> Maybe (Expr a)
forall a. a -> Maybe a
Just (a -> Expr a
forall a. Columnable a => a -> Expr a
Lit (Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
v))
            Maybe (a :~: Maybe Bool)
Nothing -> Maybe (Expr a)
forall a. Maybe a
Nothing

combineAnd :: (Columnable a) => Expr a -> Expr a -> Maybe (Expr a)
combineAnd :: forall a. Columnable a => Expr a -> Expr a -> Maybe (Expr a)
combineAnd Expr a
l Expr a
r
    | Expr a -> Expr a -> Bool
forall a. Columnable a => Expr a -> Expr a -> Bool
eqExpr Expr a
l Expr a
r = Expr a -> Maybe (Expr a)
forall a. a -> Maybe a
Just Expr a
l
    | Expr a -> Maybe Bool
forall a. Columnable a => Expr a -> Maybe Bool
asBoolLit Expr a
l Maybe Bool -> Maybe Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False = Bool -> Maybe (Expr a)
forall a. Columnable a => Bool -> Maybe (Expr a)
litBoolish Bool
False
    | Expr a -> Maybe Bool
forall a. Columnable a => Expr a -> Maybe Bool
asBoolLit Expr a
r Maybe Bool -> Maybe Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False = Bool -> Maybe (Expr a)
forall a. Columnable a => Bool -> Maybe (Expr a)
litBoolish Bool
False
    | Expr a -> Maybe Bool
forall a. Columnable a => Expr a -> Maybe Bool
asBoolLit Expr a
l Maybe Bool -> Maybe Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True = Expr a -> Maybe (Expr a)
forall a. a -> Maybe a
Just Expr a
r
    | Expr a -> Maybe Bool
forall a. Columnable a => Expr a -> Maybe Bool
asBoolLit Expr a
r Maybe Bool -> Maybe Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True = Expr a -> Maybe (Expr a)
forall a. a -> Maybe a
Just Expr a
l
    | Conn -> Expr a -> Expr a -> Bool
forall a. Columnable a => Conn -> Expr a -> Expr a -> Bool
absorbs Conn
ConnOr Expr a
l Expr a
r = Expr a -> Maybe (Expr a)
forall a. a -> Maybe a
Just Expr a
l
    | Conn -> Expr a -> Expr a -> Bool
forall a. Columnable a => Conn -> Expr a -> Expr a -> Bool
absorbs Conn
ConnOr Expr a
r Expr a
l = Expr a -> Maybe (Expr a)
forall a. a -> Maybe a
Just Expr a
r
    | Bool
otherwise = Bool -> Expr a -> Expr a -> Maybe (Expr a)
forall a.
Columnable a =>
Bool -> Expr a -> Expr a -> Maybe (Expr a)
simplifyPredicatePair Bool
True Expr a
l Expr a
r

combineOr :: (Columnable a) => Expr a -> Expr a -> Maybe (Expr a)
combineOr :: forall a. Columnable a => Expr a -> Expr a -> Maybe (Expr a)
combineOr Expr a
l Expr a
r
    | Expr a -> Expr a -> Bool
forall a. Columnable a => Expr a -> Expr a -> Bool
eqExpr Expr a
l Expr a
r = Expr a -> Maybe (Expr a)
forall a. a -> Maybe a
Just Expr a
l
    | Expr a -> Maybe Bool
forall a. Columnable a => Expr a -> Maybe Bool
asBoolLit Expr a
l Maybe Bool -> Maybe Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True = Bool -> Maybe (Expr a)
forall a. Columnable a => Bool -> Maybe (Expr a)
litBoolish Bool
True
    | Expr a -> Maybe Bool
forall a. Columnable a => Expr a -> Maybe Bool
asBoolLit Expr a
r Maybe Bool -> Maybe Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True = Bool -> Maybe (Expr a)
forall a. Columnable a => Bool -> Maybe (Expr a)
litBoolish Bool
True
    | Expr a -> Maybe Bool
forall a. Columnable a => Expr a -> Maybe Bool
asBoolLit Expr a
l Maybe Bool -> Maybe Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False = Expr a -> Maybe (Expr a)
forall a. a -> Maybe a
Just Expr a
r
    | Expr a -> Maybe Bool
forall a. Columnable a => Expr a -> Maybe Bool
asBoolLit Expr a
r Maybe Bool -> Maybe Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False = Expr a -> Maybe (Expr a)
forall a. a -> Maybe a
Just Expr a
l
    | Conn -> Expr a -> Expr a -> Bool
forall a. Columnable a => Conn -> Expr a -> Expr a -> Bool
absorbs Conn
ConnAnd Expr a
l Expr a
r = Expr a -> Maybe (Expr a)
forall a. a -> Maybe a
Just Expr a
l
    | Conn -> Expr a -> Expr a -> Bool
forall a. Columnable a => Conn -> Expr a -> Expr a -> Bool
absorbs Conn
ConnAnd Expr a
r Expr a
l = Expr a -> Maybe (Expr a)
forall a. a -> Maybe a
Just Expr a
r
    | Bool
otherwise = Bool -> Expr a -> Expr a -> Maybe (Expr a)
forall a.
Columnable a =>
Bool -> Expr a -> Expr a -> Maybe (Expr a)
simplifyPredicatePair Bool
False Expr a
l Expr a
r

absorbs :: (Columnable a) => Conn -> Expr a -> Expr a -> Bool
absorbs :: forall a. Columnable a => Conn -> Expr a -> Expr a -> Bool
absorbs Conn
conn Expr a
x (Binary (op c b a
op :: op c b a) Expr c
ya Expr b
yb)
    | Just Conn
c' <- op c b a -> Maybe Conn
forall (op :: * -> * -> * -> *) c b r.
BinaryOp op =>
op c b r -> Maybe Conn
connOf op c b a
op
    , Conn -> Conn -> Bool
sameConn Conn
conn Conn
c'
    , Just c :~: a
Refl <- TypeRep c -> TypeRep a -> Maybe (c :~: a)
forall a b. TypeRep a -> TypeRep b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @c) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @a)
    , Just b :~: a
Refl <- TypeRep b -> TypeRep a -> Maybe (b :~: a)
forall a b. TypeRep a -> TypeRep b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @b) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @a) =
        Expr a -> Expr a -> Bool
forall a. Columnable a => Expr a -> Expr a -> Bool
eqExpr Expr a
x Expr a
Expr c
ya Bool -> Bool -> Bool
|| Expr a -> Expr a -> Bool
forall a. Columnable a => Expr a -> Expr a -> Bool
eqExpr Expr a
x Expr a
Expr b
yb
absorbs Conn
_ Expr a
_ Expr a
_ = Bool
False

sameConn :: Conn -> Conn -> Bool
sameConn :: Conn -> Conn -> Bool
sameConn Conn
ConnAnd Conn
ConnAnd = Bool
True
sameConn Conn
ConnOr Conn
ConnOr = Bool
True
sameConn Conn
_ Conn
_ = Bool
False

data Cmp = CLt | CLeq | CGt | CGeq | CEq | CNeq deriving (Cmp -> Cmp -> Bool
(Cmp -> Cmp -> Bool) -> (Cmp -> Cmp -> Bool) -> Eq Cmp
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Cmp -> Cmp -> Bool
== :: Cmp -> Cmp -> Bool
$c/= :: Cmp -> Cmp -> Bool
/= :: Cmp -> Cmp -> Bool
Eq)

data NullK = Total | FalseOnNull | UnknownOnNull deriving (NullK -> NullK -> Bool
(NullK -> NullK -> Bool) -> (NullK -> NullK -> Bool) -> Eq NullK
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: NullK -> NullK -> Bool
== :: NullK -> NullK -> Bool
$c/= :: NullK -> NullK -> Bool
/= :: NullK -> NullK -> Bool
Eq)

data Atom = Atom
    { Atom -> Cmp
aCmp :: Cmp
    , Atom -> Double
aThr :: !Double
    , Atom -> String
aKey :: String
    , Atom -> NullK
aNull :: NullK
    , Atom -> Bool
aIntegral :: Bool
    }

cmpOf :: forall op c b r. (BinaryOp op) => op c b r -> Maybe Cmp
cmpOf :: forall (op :: * -> * -> * -> *) c b r.
BinaryOp op =>
op c b r -> Maybe Cmp
cmpOf op c b r
_
    | Just op :~~: NullLt
HRefl <- TypeRep op -> TypeRep NullLt -> Maybe (op :~~: NullLt)
forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
eqTypeRep (forall {k} (a :: k). Typeable a => TypeRep a
forall (a :: * -> * -> * -> *). Typeable a => TypeRep a
typeRep @op) (forall {k} (a :: k). Typeable a => TypeRep a
forall (a :: * -> * -> * -> *). Typeable a => TypeRep a
typeRep @NullLt) = Cmp -> Maybe Cmp
forall a. a -> Maybe a
Just Cmp
CLt
    | Just op :~~: NullLeq
HRefl <- TypeRep op -> TypeRep NullLeq -> Maybe (op :~~: NullLeq)
forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
eqTypeRep (forall {k} (a :: k). Typeable a => TypeRep a
forall (a :: * -> * -> * -> *). Typeable a => TypeRep a
typeRep @op) (forall {k} (a :: k). Typeable a => TypeRep a
forall (a :: * -> * -> * -> *). Typeable a => TypeRep a
typeRep @NullLeq) = Cmp -> Maybe Cmp
forall a. a -> Maybe a
Just Cmp
CLeq
    | Just op :~~: NullGt
HRefl <- TypeRep op -> TypeRep NullGt -> Maybe (op :~~: NullGt)
forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
eqTypeRep (forall {k} (a :: k). Typeable a => TypeRep a
forall (a :: * -> * -> * -> *). Typeable a => TypeRep a
typeRep @op) (forall {k} (a :: k). Typeable a => TypeRep a
forall (a :: * -> * -> * -> *). Typeable a => TypeRep a
typeRep @NullGt) = Cmp -> Maybe Cmp
forall a. a -> Maybe a
Just Cmp
CGt
    | Just op :~~: NullGeq
HRefl <- TypeRep op -> TypeRep NullGeq -> Maybe (op :~~: NullGeq)
forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
eqTypeRep (forall {k} (a :: k). Typeable a => TypeRep a
forall (a :: * -> * -> * -> *). Typeable a => TypeRep a
typeRep @op) (forall {k} (a :: k). Typeable a => TypeRep a
forall (a :: * -> * -> * -> *). Typeable a => TypeRep a
typeRep @NullGeq) = Cmp -> Maybe Cmp
forall a. a -> Maybe a
Just Cmp
CGeq
    | Just op :~~: NullEq
HRefl <- TypeRep op -> TypeRep NullEq -> Maybe (op :~~: NullEq)
forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
eqTypeRep (forall {k} (a :: k). Typeable a => TypeRep a
forall (a :: * -> * -> * -> *). Typeable a => TypeRep a
typeRep @op) (forall {k} (a :: k). Typeable a => TypeRep a
forall (a :: * -> * -> * -> *). Typeable a => TypeRep a
typeRep @NullEq) = Cmp -> Maybe Cmp
forall a. a -> Maybe a
Just Cmp
CEq
    | Just op :~~: NullNeq
HRefl <- TypeRep op -> TypeRep NullNeq -> Maybe (op :~~: NullNeq)
forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
eqTypeRep (forall {k} (a :: k). Typeable a => TypeRep a
forall (a :: * -> * -> * -> *). Typeable a => TypeRep a
typeRep @op) (forall {k} (a :: k). Typeable a => TypeRep a
forall (a :: * -> * -> * -> *). Typeable a => TypeRep a
typeRep @NullNeq) = Cmp -> Maybe Cmp
forall a. a -> Maybe a
Just Cmp
CNeq
    | Bool
otherwise = Maybe Cmp
forall a. Maybe a
Nothing

isLower, isUpper :: Cmp -> Bool
isLower :: Cmp -> Bool
isLower Cmp
c = Cmp
c Cmp -> Cmp -> Bool
forall a. Eq a => a -> a -> Bool
== Cmp
CGt Bool -> Bool -> Bool
|| Cmp
c Cmp -> Cmp -> Bool
forall a. Eq a => a -> a -> Bool
== Cmp
CGeq
isUpper :: Cmp -> Bool
isUpper Cmp
c = Cmp
c Cmp -> Cmp -> Bool
forall a. Eq a => a -> a -> Bool
== Cmp
CLt Bool -> Bool -> Bool
|| Cmp
c Cmp -> Cmp -> Bool
forall a. Eq a => a -> a -> Bool
== Cmp
CLeq

-- | True if @x@ is a @Maybe _@ type.
isMaybeTy :: forall x. (Columnable x) => Bool
isMaybeTy :: forall a. Columnable a => Bool
isMaybeTy = case forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @x of
    App TypeRep a
con TypeRep b
_ -> case TypeRep a -> TypeRep Maybe -> Maybe (a :~~: Maybe)
forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
eqTypeRep TypeRep a
con (forall {k} (a :: k). Typeable a => TypeRep a
forall (a :: * -> *). Typeable a => TypeRep a
typeRep @Maybe) of Just a :~~: Maybe
HRefl -> Bool
True; Maybe (a :~~: Maybe)
_ -> Bool
False
    TypeRep x
_ -> Bool
False

litDouble :: forall b. (Columnable b) => Expr b -> Maybe Double
litDouble :: forall b. Columnable b => Expr b -> Maybe Double
litDouble (Lit b
v) =
    case TypeRep b -> TypeRep Double -> Maybe (b :~: Double)
forall a b. TypeRep a -> TypeRep b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @b) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @Double) of
        Just b :~: Double
Refl -> Double -> Maybe Double
forall a. a -> Maybe a
Just b
Double
v
        Maybe (b :~: Double)
Nothing -> case TypeRep b -> TypeRep Int -> Maybe (b :~: Int)
forall a b. TypeRep a -> TypeRep b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @b) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @Int) of
            Just b :~: Int
Refl -> Double -> Maybe Double
forall a. a -> Maybe a
Just (b -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral b
v)
            Maybe (b :~: Int)
Nothing -> case TypeRep b -> TypeRep (Maybe Double) -> Maybe (b :~: Maybe Double)
forall a b. TypeRep a -> TypeRep b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @b) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @(Maybe Double)) of
                Just b :~: Maybe Double
Refl -> b
Maybe Double
v
                Maybe (b :~: Maybe Double)
Nothing -> case TypeRep b -> TypeRep (Maybe Int) -> Maybe (b :~: Maybe Int)
forall a b. TypeRep a -> TypeRep b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @b) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @(Maybe Int)) of
                    Just b :~: Maybe Int
Refl -> Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Double) -> Maybe Int -> Maybe Double
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> b
Maybe Int
v
                    Maybe (b :~: Maybe Int)
Nothing -> Maybe Double
forall a. Maybe a
Nothing
litDouble Expr b
_ = Maybe Double
forall a. Maybe a
Nothing

{- | True for a column lifted from an integral type (never NaN): @toDouble (col …)@
or a column whose type is itself integral.
-}
integralColE :: forall c. (Columnable c) => Expr c -> Bool
integralColE :: forall c. Columnable c => Expr c -> Bool
integralColE (Unary op b c
op Expr b
_) = op b c -> Text
forall a b. op a b -> Text
forall (op :: * -> * -> *) a b. UnaryOp op => op a b -> Text
unaryName op b c
op Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
"toDouble"
integralColE Expr c
_ =
    [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or
        [ forall a. Columnable a => Bool
matches @Int
        , forall a. Columnable a => Bool
matches @(Maybe Int)
        ]
  where
    matches :: forall t. (Columnable t) => Bool
    matches :: forall a. Columnable a => Bool
matches = case TypeRep c -> TypeRep t -> Maybe (c :~: t)
forall a b. TypeRep a -> TypeRep b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @c) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @t) of Just c :~: t
Refl -> Bool
True; Maybe (c :~: t)
_ -> Bool
False

atomOf :: forall a. (Columnable a) => Expr a -> Maybe Atom
atomOf :: forall a. Columnable a => Expr a -> Maybe Atom
atomOf (Unary op b a
fm (Binary (op c b b
op :: op c b r) (Expr c
colE :: Expr c) Expr b
litE))
    | op b a -> Text
forall a b. op a b -> Text
forall (op :: * -> * -> *) a b. UnaryOp op => op a b -> Text
unaryName op b a
fm Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
"fromMaybe"
    , Just Cmp
cmp <- op c b b -> Maybe Cmp
forall (op :: * -> * -> * -> *) c b r.
BinaryOp op =>
op c b r -> Maybe Cmp
cmpOf op c b b
op
    , Just Double
t <- Expr b -> Maybe Double
forall b. Columnable b => Expr b -> Maybe Double
litDouble Expr b
litE =
        Atom -> Maybe Atom
forall a. a -> Maybe a
Just (Cmp -> Double -> String -> NullK -> Bool -> Atom
Atom Cmp
cmp Double
t (Expr c -> String
forall a. Show a => a -> String
show (Expr c -> Expr c
forall a. (Show a, Typeable a) => Expr a -> Expr a
normalize Expr c
colE)) NullK
FalseOnNull (Expr c -> Bool
forall c. Columnable c => Expr c -> Bool
integralColE Expr c
colE))
atomOf (Binary (op c b a
op :: op c b a) (Expr c
colE :: Expr c) Expr b
litE)
    | Just Cmp
cmp <- op c b a -> Maybe Cmp
forall (op :: * -> * -> * -> *) c b r.
BinaryOp op =>
op c b r -> Maybe Cmp
cmpOf op c b a
op
    , Just Double
t <- Expr b -> Maybe Double
forall b. Columnable b => Expr b -> Maybe Double
litDouble Expr b
litE =
        let nk :: NullK
nk = if forall a. Columnable a => Bool
isMaybeTy @c then NullK
UnknownOnNull else NullK
Total
         in Atom -> Maybe Atom
forall a. a -> Maybe a
Just (Cmp -> Double -> String -> NullK -> Bool -> Atom
Atom Cmp
cmp Double
t (Expr c -> String
forall a. Show a => a -> String
show (Expr c -> Expr c
forall a. (Show a, Typeable a) => Expr a -> Expr a
normalize Expr c
colE)) NullK
nk (Expr c -> Bool
forall c. Columnable c => Expr c -> Bool
integralColE Expr c
colE))
atomOf Expr a
_ = Maybe Atom
forall a. Maybe a
Nothing

simplifyPredicatePair ::
    forall a. (Columnable a) => Bool -> Expr a -> Expr a -> Maybe (Expr a)
simplifyPredicatePair :: forall a.
Columnable a =>
Bool -> Expr a -> Expr a -> Maybe (Expr a)
simplifyPredicatePair Bool
isAnd Expr a
a Expr a
b = do
    Atom
atomA <- Expr a -> Maybe Atom
forall a. Columnable a => Expr a -> Maybe Atom
atomOf Expr a
a
    Atom
atomB <- Expr a -> Maybe Atom
forall a. Columnable a => Expr a -> Maybe Atom
atomOf Expr a
b
    Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Atom -> String
aKey Atom
atomA String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== Atom -> String
aKey Atom
atomB)
    let nk :: NullK
nk = Atom -> NullK
aNull Atom
atomA
        integral :: Bool
integral = Atom -> Bool
aIntegral Atom
atomA
    if Bool
isAnd
        then Expr a -> Atom -> Expr a -> Atom -> NullK -> Bool -> Maybe (Expr a)
forall a.
Columnable a =>
Expr a -> Atom -> Expr a -> Atom -> NullK -> Bool -> Maybe (Expr a)
andAtoms Expr a
a Atom
atomA Expr a
b Atom
atomB NullK
nk Bool
integral
        else Expr a -> Atom -> Expr a -> Atom -> NullK -> Bool -> Maybe (Expr a)
forall a.
Columnable a =>
Expr a -> Atom -> Expr a -> Atom -> NullK -> Bool -> Maybe (Expr a)
orAtoms Expr a
a Atom
atomA Expr a
b Atom
atomB NullK
nk Bool
integral

-- | Contradiction folds to a literal False unless null-rows make it unknown.
litFalseGated :: (Columnable a) => NullK -> Maybe (Expr a)
litFalseGated :: forall a. Columnable a => NullK -> Maybe (Expr a)
litFalseGated NullK
UnknownOnNull = Maybe (Expr a)
forall a. Maybe a
Nothing
litFalseGated NullK
_ = Bool -> Maybe (Expr a)
forall a. Columnable a => Bool -> Maybe (Expr a)
litBoolish Bool
False

{- | Tautology to literal True is sound only for total (never-null) atoms; the
exhaustive-cover form additionally needs a non-NaN (integral) column.
-}
litTrueTotal :: (Columnable a) => NullK -> Maybe (Expr a)
litTrueTotal :: forall a. Columnable a => NullK -> Maybe (Expr a)
litTrueTotal NullK
Total = Bool -> Maybe (Expr a)
forall a. Columnable a => Bool -> Maybe (Expr a)
litBoolish Bool
True
litTrueTotal NullK
_ = Maybe (Expr a)
forall a. Maybe a
Nothing

andAtoms ::
    (Columnable a) =>
    Expr a -> Atom -> Expr a -> Atom -> NullK -> Bool -> Maybe (Expr a)
andAtoms :: forall a.
Columnable a =>
Expr a -> Atom -> Expr a -> Atom -> NullK -> Bool -> Maybe (Expr a)
andAtoms Expr a
a Atom
atomA Expr a
b Atom
atomB NullK
nk Bool
_ =
    let cA :: Cmp
cA = Atom -> Cmp
aCmp Atom
atomA; tA :: Double
tA = Atom -> Double
aThr Atom
atomA; cB :: Cmp
cB = Atom -> Cmp
aCmp Atom
atomB; tB :: Double
tB = Atom -> Double
aThr Atom
atomB
     in if
            | Cmp -> Bool
isLower Cmp
cA, Cmp -> Bool
isLower Cmp
cB, Cmp
cA Cmp -> Cmp -> Bool
forall a. Eq a => a -> a -> Bool
== Cmp
cB -> Expr a -> Maybe (Expr a)
forall a. a -> Maybe a
Just (if Double
tA Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
>= Double
tB then Expr a
a else Expr a
b)
            | Cmp -> Bool
isUpper Cmp
cA, Cmp -> Bool
isUpper Cmp
cB, Cmp
cA Cmp -> Cmp -> Bool
forall a. Eq a => a -> a -> Bool
== Cmp
cB -> Expr a -> Maybe (Expr a)
forall a. a -> Maybe a
Just (if Double
tA Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
<= Double
tB then Expr a
a else Expr a
b)
            | Cmp -> Bool
isLower Cmp
cA, Cmp -> Bool
isUpper Cmp
cB -> Cmp -> Double -> Cmp -> Double -> Maybe (Expr a)
lu Cmp
cA Double
tA Cmp
cB Double
tB
            | Cmp -> Bool
isUpper Cmp
cA, Cmp -> Bool
isLower Cmp
cB -> Cmp -> Double -> Cmp -> Double -> Maybe (Expr a)
lu Cmp
cB Double
tB Cmp
cA Double
tA
            | Cmp
cA Cmp -> Cmp -> Bool
forall a. Eq a => a -> a -> Bool
== Cmp
CEq, Cmp
cB Cmp -> Cmp -> Bool
forall a. Eq a => a -> a -> Bool
== Cmp
CEq -> if Double
tA Double -> Double -> Bool
forall a. Eq a => a -> a -> Bool
== Double
tB then Expr a -> Maybe (Expr a)
forall a. a -> Maybe a
Just Expr a
a else NullK -> Maybe (Expr a)
forall a. Columnable a => NullK -> Maybe (Expr a)
litFalseGated NullK
nk
            | Cmp
cA Cmp -> Cmp -> Bool
forall a. Eq a => a -> a -> Bool
== Cmp
CEq, Cmp
cB Cmp -> Cmp -> Bool
forall a. Eq a => a -> a -> Bool
== Cmp
CNeq -> if Double
tA Double -> Double -> Bool
forall a. Eq a => a -> a -> Bool
== Double
tB then NullK -> Maybe (Expr a)
forall a. Columnable a => NullK -> Maybe (Expr a)
litFalseGated NullK
nk else Expr a -> Maybe (Expr a)
forall a. a -> Maybe a
Just Expr a
a
            | Cmp
cA Cmp -> Cmp -> Bool
forall a. Eq a => a -> a -> Bool
== Cmp
CNeq, Cmp
cB Cmp -> Cmp -> Bool
forall a. Eq a => a -> a -> Bool
== Cmp
CEq -> if Double
tA Double -> Double -> Bool
forall a. Eq a => a -> a -> Bool
== Double
tB then NullK -> Maybe (Expr a)
forall a. Columnable a => NullK -> Maybe (Expr a)
litFalseGated NullK
nk else Expr a -> Maybe (Expr a)
forall a. a -> Maybe a
Just Expr a
b
            | Cmp
cA Cmp -> Cmp -> Bool
forall a. Eq a => a -> a -> Bool
== Cmp
CEq -> if Double -> Cmp -> Double -> Bool
satisfies Double
tA Cmp
cB Double
tB then Expr a -> Maybe (Expr a)
forall a. a -> Maybe a
Just Expr a
a else NullK -> Maybe (Expr a)
forall a. Columnable a => NullK -> Maybe (Expr a)
litFalseGated NullK
nk
            | Cmp
cB Cmp -> Cmp -> Bool
forall a. Eq a => a -> a -> Bool
== Cmp
CEq -> if Double -> Cmp -> Double -> Bool
satisfies Double
tB Cmp
cA Double
tA then Expr a -> Maybe (Expr a)
forall a. a -> Maybe a
Just Expr a
b else NullK -> Maybe (Expr a)
forall a. Columnable a => NullK -> Maybe (Expr a)
litFalseGated NullK
nk
            | Cmp
cA Cmp -> Cmp -> Bool
forall a. Eq a => a -> a -> Bool
== Cmp
CNeq, Cmp
cB Cmp -> Cmp -> Bool
forall a. Eq a => a -> a -> Bool
== Cmp
CNeq -> Maybe (Expr a)
forall a. Maybe a
Nothing
            | Cmp
cA Cmp -> Cmp -> Bool
forall a. Eq a => a -> a -> Bool
== Cmp
CNeq -> if Double -> Cmp -> Double -> Bool
outside Double
tA Cmp
cB Double
tB then Expr a -> Maybe (Expr a)
forall a. a -> Maybe a
Just Expr a
b else Maybe (Expr a)
forall a. Maybe a
Nothing
            | Cmp
cB Cmp -> Cmp -> Bool
forall a. Eq a => a -> a -> Bool
== Cmp
CNeq -> if Double -> Cmp -> Double -> Bool
outside Double
tB Cmp
cA Double
tA then Expr a -> Maybe (Expr a)
forall a. a -> Maybe a
Just Expr a
a else Maybe (Expr a)
forall a. Maybe a
Nothing
            | Bool
otherwise -> Maybe (Expr a)
forall a. Maybe a
Nothing
  where
    lu :: Cmp -> Double -> Cmp -> Double -> Maybe (Expr a)
lu Cmp
lc Double
lo Cmp
uc Double
hi
        | Double
lo Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
> Double
hi = NullK -> Maybe (Expr a)
forall a. Columnable a => NullK -> Maybe (Expr a)
litFalseGated NullK
nk
        | Double
lo Double -> Double -> Bool
forall a. Eq a => a -> a -> Bool
== Double
hi, Cmp
lc Cmp -> Cmp -> Bool
forall a. Eq a => a -> a -> Bool
== Cmp
CGeq, Cmp
uc Cmp -> Cmp -> Bool
forall a. Eq a => a -> a -> Bool
== Cmp
CLeq = Expr a -> Double -> Maybe (Expr a)
forall a. Columnable a => Expr a -> Double -> Maybe (Expr a)
pointEq Expr a
a Double
lo
        | Double
lo Double -> Double -> Bool
forall a. Eq a => a -> a -> Bool
== Double
hi = NullK -> Maybe (Expr a)
forall a. Columnable a => NullK -> Maybe (Expr a)
litFalseGated NullK
nk
        | Bool
otherwise = Maybe (Expr a)
forall a. Maybe a
Nothing

orAtoms ::
    (Columnable a) =>
    Expr a -> Atom -> Expr a -> Atom -> NullK -> Bool -> Maybe (Expr a)
orAtoms :: forall a.
Columnable a =>
Expr a -> Atom -> Expr a -> Atom -> NullK -> Bool -> Maybe (Expr a)
orAtoms Expr a
a Atom
atomA Expr a
b Atom
atomB NullK
nk Bool
integral =
    let cA :: Cmp
cA = Atom -> Cmp
aCmp Atom
atomA; tA :: Double
tA = Atom -> Double
aThr Atom
atomA; cB :: Cmp
cB = Atom -> Cmp
aCmp Atom
atomB; tB :: Double
tB = Atom -> Double
aThr Atom
atomB
     in if
            | Cmp -> Bool
isLower Cmp
cA, Cmp -> Bool
isLower Cmp
cB, Cmp
cA Cmp -> Cmp -> Bool
forall a. Eq a => a -> a -> Bool
== Cmp
cB -> Expr a -> Maybe (Expr a)
forall a. a -> Maybe a
Just (if Double
tA Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
<= Double
tB then Expr a
a else Expr a
b)
            | Cmp -> Bool
isUpper Cmp
cA, Cmp -> Bool
isUpper Cmp
cB, Cmp
cA Cmp -> Cmp -> Bool
forall a. Eq a => a -> a -> Bool
== Cmp
cB -> Expr a -> Maybe (Expr a)
forall a. a -> Maybe a
Just (if Double
tA Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
>= Double
tB then Expr a
a else Expr a
b)
            | Cmp -> Bool
isUpper Cmp
cA
            , Cmp -> Bool
isLower Cmp
cB
            , NullK
nk NullK -> NullK -> Bool
forall a. Eq a => a -> a -> Bool
== NullK
Total
            , Bool
integral
            , Cmp -> Double -> Cmp -> Double -> Bool
covers Cmp
cB Double
tB Cmp
cA Double
tA ->
                NullK -> Maybe (Expr a)
forall a. Columnable a => NullK -> Maybe (Expr a)
litTrueTotal NullK
nk
            | Cmp -> Bool
isLower Cmp
cA
            , Cmp -> Bool
isUpper Cmp
cB
            , NullK
nk NullK -> NullK -> Bool
forall a. Eq a => a -> a -> Bool
== NullK
Total
            , Bool
integral
            , Cmp -> Double -> Cmp -> Double -> Bool
covers Cmp
cA Double
tA Cmp
cB Double
tB ->
                NullK -> Maybe (Expr a)
forall a. Columnable a => NullK -> Maybe (Expr a)
litTrueTotal NullK
nk
            | Cmp
cA Cmp -> Cmp -> Bool
forall a. Eq a => a -> a -> Bool
== Cmp
CNeq, Cmp
cB Cmp -> Cmp -> Bool
forall a. Eq a => a -> a -> Bool
== Cmp
CNeq -> if Double
tA Double -> Double -> Bool
forall a. Eq a => a -> a -> Bool
== Double
tB then Expr a -> Maybe (Expr a)
forall a. a -> Maybe a
Just Expr a
a else NullK -> Maybe (Expr a)
forall a. Columnable a => NullK -> Maybe (Expr a)
litTrueTotal NullK
nk
            | Cmp
cA Cmp -> Cmp -> Bool
forall a. Eq a => a -> a -> Bool
== Cmp
CEq, Cmp
cB Cmp -> Cmp -> Bool
forall a. Eq a => a -> a -> Bool
== Cmp
CNeq -> if Double
tA Double -> Double -> Bool
forall a. Eq a => a -> a -> Bool
== Double
tB then NullK -> Maybe (Expr a)
forall a. Columnable a => NullK -> Maybe (Expr a)
litTrueTotal NullK
nk else Expr a -> Maybe (Expr a)
forall a. a -> Maybe a
Just Expr a
b
            | Cmp
cA Cmp -> Cmp -> Bool
forall a. Eq a => a -> a -> Bool
== Cmp
CNeq, Cmp
cB Cmp -> Cmp -> Bool
forall a. Eq a => a -> a -> Bool
== Cmp
CEq -> if Double
tA Double -> Double -> Bool
forall a. Eq a => a -> a -> Bool
== Double
tB then NullK -> Maybe (Expr a)
forall a. Columnable a => NullK -> Maybe (Expr a)
litTrueTotal NullK
nk else Expr a -> Maybe (Expr a)
forall a. a -> Maybe a
Just Expr a
a
            | Cmp
cA Cmp -> Cmp -> Bool
forall a. Eq a => a -> a -> Bool
== Cmp
CEq, Cmp
cB Cmp -> Cmp -> Bool
forall a. Eq a => a -> a -> Bool
== Cmp
CEq -> if Double
tA Double -> Double -> Bool
forall a. Eq a => a -> a -> Bool
== Double
tB then Expr a -> Maybe (Expr a)
forall a. a -> Maybe a
Just Expr a
a else Maybe (Expr a)
forall a. Maybe a
Nothing
            | Bool
otherwise -> Maybe (Expr a)
forall a. Maybe a
Nothing

{- | Build @col == t@ for the point-collapse rule; only strict @Expr Bool@ over a
@Double@ column (otherwise bail).
-}
pointEq :: forall a. (Columnable a) => Expr a -> Double -> Maybe (Expr a)
pointEq :: forall a. Columnable a => Expr a -> Double -> Maybe (Expr a)
pointEq Expr a
atom Double
lo = case TypeRep a -> TypeRep Bool -> Maybe (a :~: Bool)
forall a b. TypeRep a -> TypeRep b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @a) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @Bool) of
    Just a :~: Bool
Refl -> (\Expr Double
colE -> Expr Double
colE Expr Double -> Expr Double -> Expr Bool
forall a. (Columnable a, Eq a) => Expr a -> Expr a -> Expr Bool
.==. Double -> Expr Double
forall a. Columnable a => a -> Expr a
Lit Double
lo) (Expr Double -> Expr a) -> Maybe (Expr Double) -> Maybe (Expr a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr a -> Maybe (Expr Double)
forall x. Expr x -> Maybe (Expr Double)
recoverColD Expr a
atom
    Maybe (a :~: Bool)
Nothing -> Maybe (Expr a)
forall a. Maybe a
Nothing

recoverColD :: Expr x -> Maybe (Expr Double)
recoverColD :: forall x. Expr x -> Maybe (Expr Double)
recoverColD (Binary op c b x
_ (Expr c
colE :: Expr c) Expr b
_) =
    case TypeRep c -> TypeRep Double -> Maybe (c :~: Double)
forall a b. TypeRep a -> TypeRep b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @c) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @Double) of
        Just c :~: Double
Refl -> Expr Double -> Maybe (Expr Double)
forall a. a -> Maybe a
Just Expr c
Expr Double
colE
        Maybe (c :~: Double)
_ -> Maybe (Expr Double)
forall a. Maybe a
Nothing
recoverColD (Unary op b x
_ Expr b
inner) = Expr b -> Maybe (Expr Double)
forall x. Expr x -> Maybe (Expr Double)
recoverColD Expr b
inner
recoverColD Expr x
_ = Maybe (Expr Double)
forall a. Maybe a
Nothing

covers :: Cmp -> Double -> Cmp -> Double -> Bool
covers :: Cmp -> Double -> Cmp -> Double -> Bool
covers Cmp
lowerCmp Double
lo Cmp
upperCmp Double
hi =
    Double
lo Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
< Double
hi Bool -> Bool -> Bool
|| (Double
lo Double -> Double -> Bool
forall a. Eq a => a -> a -> Bool
== Double
hi Bool -> Bool -> Bool
&& (Cmp
lowerCmp Cmp -> Cmp -> Bool
forall a. Eq a => a -> a -> Bool
== Cmp
CGeq Bool -> Bool -> Bool
|| Cmp
upperCmp Cmp -> Cmp -> Bool
forall a. Eq a => a -> a -> Bool
== Cmp
CLeq))

satisfies :: Double -> Cmp -> Double -> Bool
satisfies :: Double -> Cmp -> Double -> Bool
satisfies Double
t Cmp
CGt Double
tb = Double
t Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
> Double
tb
satisfies Double
t Cmp
CGeq Double
tb = Double
t Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
>= Double
tb
satisfies Double
t Cmp
CLt Double
tb = Double
t Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
< Double
tb
satisfies Double
t Cmp
CLeq Double
tb = Double
t Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
<= Double
tb
satisfies Double
_ Cmp
_ Double
_ = Bool
False

outside :: Double -> Cmp -> Double -> Bool
outside :: Double -> Cmp -> Double -> Bool
outside Double
t Cmp
CGt Double
tb = Double
t Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
<= Double
tb
outside Double
t Cmp
CGeq Double
tb = Double
t Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
< Double
tb
outside Double
t Cmp
CLt Double
tb = Double
t Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
>= Double
tb
outside Double
t Cmp
CLeq Double
tb = Double
t Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
> Double
tb
outside Double
_ Cmp
_ Double
_ = Bool
False

-- ---------------------------------------------------------------------------
-- Path-condition entailment for fitted-tree pruning.
-- ---------------------------------------------------------------------------

-- | A known same-column threshold fact accumulated along a tree path.
data PredFact = PredFact !String !Cmp !Double

-- | The fact a branch's true edge establishes (the condition holds).
factTrue :: Expr Bool -> Maybe PredFact
factTrue :: Expr Bool -> Maybe PredFact
factTrue Expr Bool
e = (\Atom
a -> String -> Cmp -> Double -> PredFact
PredFact (Atom -> String
aKey Atom
a) (Atom -> Cmp
aCmp Atom
a) (Atom -> Double
aThr Atom
a)) (Atom -> PredFact) -> Maybe Atom -> Maybe PredFact
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr Bool -> Maybe Atom
forall a. Columnable a => Expr a -> Maybe Atom
atomOf Expr Bool
e

{- | The fact a branch's false edge establishes (the negated condition). Only
sound for non-NaN (integral) columns — a NaN row takes the false edge too,
so @¬(x>t)@ is not a clean @x<=t@ bound for floats.
-}
factFalse :: Expr Bool -> Maybe PredFact
factFalse :: Expr Bool -> Maybe PredFact
factFalse Expr Bool
e = do
    Atom
a <- Expr Bool -> Maybe Atom
forall a. Columnable a => Expr a -> Maybe Atom
atomOf Expr Bool
e
    Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Atom -> Bool
aIntegral Atom
a Bool -> Bool -> Bool
&& Atom -> NullK
aNull Atom
a NullK -> NullK -> Bool
forall a. Eq a => a -> a -> Bool
== NullK
Total)
    Cmp
nc <- Cmp -> Maybe Cmp
negCmp (Atom -> Cmp
aCmp Atom
a)
    PredFact -> Maybe PredFact
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Cmp -> Double -> PredFact
PredFact (Atom -> String
aKey Atom
a) Cmp
nc (Atom -> Double
aThr Atom
a))

negCmp :: Cmp -> Maybe Cmp
negCmp :: Cmp -> Maybe Cmp
negCmp Cmp
CLt = Cmp -> Maybe Cmp
forall a. a -> Maybe a
Just Cmp
CGeq
negCmp Cmp
CLeq = Cmp -> Maybe Cmp
forall a. a -> Maybe a
Just Cmp
CGt
negCmp Cmp
CGt = Cmp -> Maybe Cmp
forall a. a -> Maybe a
Just Cmp
CLeq
negCmp Cmp
CGeq = Cmp -> Maybe Cmp
forall a. a -> Maybe a
Just Cmp
CLt
negCmp Cmp
_ = Maybe Cmp
forall a. Maybe a
Nothing

{- | @entails facts cond@: 'Just' 'True' when the path facts force @cond@ true,
'Just' 'False' when they force it false, 'Nothing' when undecided.
-}
entails :: [PredFact] -> Expr Bool -> Maybe Bool
entails :: [PredFact] -> Expr Bool -> Maybe Bool
entails [PredFact]
facts Expr Bool
cond = do
    Atom
a <- Expr Bool -> Maybe Atom
forall a. Columnable a => Expr a -> Maybe Atom
atomOf Expr Bool
cond
    let decisions :: [Bool]
decisions =
            [ Bool
d
            | PredFact String
fk Cmp
fc Double
ft <- [PredFact]
facts
            , String
fk String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== Atom -> String
aKey Atom
a
            , Just Bool
d <- [(Cmp, Double) -> (Cmp, Double) -> Maybe Bool
factImplies (Cmp
fc, Double
ft) (Atom -> Cmp
aCmp Atom
a, Atom -> Double
aThr Atom
a)]
            ]
    case [Bool]
decisions of
        (Bool
d : [Bool]
_) -> Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
d
        [] -> Maybe Bool
forall a. Maybe a
Nothing

{- | Does the fact's solution set sit inside @cond@ ('Just' 'True'), disjoint
from it ('Just' 'False'), or neither ('Nothing')? Boundary strictness is
honoured: e.g. @x<=t@ does NOT entail @x<t@, and @x>=t ∧ x<=t@ is not empty.
-}
factImplies :: (Cmp, Double) -> (Cmp, Double) -> Maybe Bool
factImplies :: (Cmp, Double) -> (Cmp, Double) -> Maybe Bool
factImplies (Cmp
fc, Double
ft) (Cmp
cc, Double
tc)
    | Cmp -> Bool
isLower Cmp
fc, Cmp -> Bool
isLower Cmp
cc, Bool
subset = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True
    | Cmp -> Bool
isUpper Cmp
fc, Cmp -> Bool
isUpper Cmp
cc, Bool
subset = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True
    | Cmp -> Bool
isLower Cmp
fc, Cmp -> Bool
isUpper Cmp
cc, Bool
disjointAtEq = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
    | Cmp -> Bool
isUpper Cmp
fc, Cmp -> Bool
isLower Cmp
cc, Bool
disjointBelow = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
    | Bool
otherwise = Maybe Bool
forall a. Maybe a
Nothing
  where
    fIncl :: Bool
fIncl = Cmp
fc Cmp -> Cmp -> Bool
forall a. Eq a => a -> a -> Bool
== Cmp
CGeq Bool -> Bool -> Bool
|| Cmp
fc Cmp -> Cmp -> Bool
forall a. Eq a => a -> a -> Bool
== Cmp
CLeq
    cIncl :: Bool
cIncl = Cmp
cc Cmp -> Cmp -> Bool
forall a. Eq a => a -> a -> Bool
== Cmp
CGeq Bool -> Bool -> Bool
|| Cmp
cc Cmp -> Cmp -> Bool
forall a. Eq a => a -> a -> Bool
== Cmp
CLeq
    subset :: Bool
subset =
        (if Cmp -> Bool
isLower Cmp
fc then Double
ft Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
> Double
tc else Double
ft Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
< Double
tc)
            Bool -> Bool -> Bool
|| (Double
ft Double -> Double -> Bool
forall a. Eq a => a -> a -> Bool
== Double
tc Bool -> Bool -> Bool
&& (Bool -> Bool
not Bool
fIncl Bool -> Bool -> Bool
|| Bool
cIncl))
    disjointAtEq :: Bool
disjointAtEq = Double
ft Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
> Double
tc Bool -> Bool -> Bool
|| (Double
ft Double -> Double -> Bool
forall a. Eq a => a -> a -> Bool
== Double
tc Bool -> Bool -> Bool
&& Bool -> Bool
not (Bool
fIncl Bool -> Bool -> Bool
&& Bool
cIncl))
    disjointBelow :: Bool
disjointBelow = Double
ft Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
< Double
tc Bool -> Bool -> Bool
|| (Double
ft Double -> Double -> Bool
forall a. Eq a => a -> a -> Bool
== Double
tc Bool -> Bool -> Bool
&& Bool -> Bool
not (Bool
fIncl Bool -> Bool -> Bool
&& Bool
cIncl))