{-# OPTIONS_GHC -Wno-orphans #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeFamilies #-}

--------------------------------------------------------------------------------
-- | Boolean formulas without quantifiers and without negation.
-- Such a formula consists of variables, conjunctions (and), and disjunctions (or).
--
-- This module is used to represent minimal complete definitions for classes.
--
module GHC.Data.BooleanFormula (
        module Language.Haskell.Syntax.BooleanFormula,
        isFalse, isTrue,
        bfMap, bfTraverse,
        eval, simplify, isUnsatisfied,
        implies, impliesAtom,
        pprBooleanFormula, pprBooleanFormulaNice, pprBooleanFormulaNormal
  ) where

import Data.List ( intersperse )
import Data.List.NonEmpty ( NonEmpty (..), init, last )

import GHC.Prelude hiding ( init, last )
import GHC.Types.Unique
import GHC.Types.Unique.Set
import GHC.Types.SrcLoc (unLoc)
import GHC.Utils.Outputable
import GHC.Parser.Annotation ( SrcSpanAnnL )
import GHC.Hs.Extension (GhcPass (..), OutputableBndrId)
import Language.Haskell.Syntax.Extension (Anno, LIdP, IdP)
import Language.Haskell.Syntax.BooleanFormula


----------------------------------------------------------------------
-- Boolean formula type and smart constructors
----------------------------------------------------------------------

type instance Anno (BooleanFormula (GhcPass p)) = SrcSpanAnnL

-- if we had Functor/Traversable (LbooleanFormula p) we could use that
-- as a constraint and we wouldn't need to specialize to just GhcPass p,
-- but becuase LBooleanFormula is a type synonym such a constraint is
-- impossible.

-- BooleanFormula can't be an instance of functor because it can't lift
-- arbitrary functions `a -> b`, only functions of type `LIdP a -> LIdP b`
-- ditto for Traversable.
bfMap :: (LIdP (GhcPass p) -> LIdP (GhcPass p'))
      -> BooleanFormula (GhcPass p) -> BooleanFormula (GhcPass p')
bfMap :: forall (p :: Pass) (p' :: Pass).
(LIdP (GhcPass p) -> LIdP (GhcPass p'))
-> BooleanFormula (GhcPass p) -> BooleanFormula (GhcPass p')
bfMap LIdP (GhcPass p) -> LIdP (GhcPass p')
f = BooleanFormula (GhcPass p) -> BooleanFormula (GhcPass p')
go
  where
    go :: BooleanFormula (GhcPass p) -> BooleanFormula (GhcPass p')
go (Var    LIdP (GhcPass p)
a  ) = LIdP (GhcPass p') -> BooleanFormula (GhcPass p')
forall p. LIdP p -> BooleanFormula p
Var     (LIdP (GhcPass p') -> BooleanFormula (GhcPass p'))
-> LIdP (GhcPass p') -> BooleanFormula (GhcPass p')
forall a b. (a -> b) -> a -> b
$ LIdP (GhcPass p) -> LIdP (GhcPass p')
f LIdP (GhcPass p)
a
    go (And    [LBooleanFormula (GhcPass p)]
bfs) = [LBooleanFormula (GhcPass p')] -> BooleanFormula (GhcPass p')
forall p. [LBooleanFormula p] -> BooleanFormula p
And     ([LBooleanFormula (GhcPass p')] -> BooleanFormula (GhcPass p'))
-> [LBooleanFormula (GhcPass p')] -> BooleanFormula (GhcPass p')
forall a b. (a -> b) -> a -> b
$ (GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p))
 -> LBooleanFormula (GhcPass p'))
-> [GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p))]
-> [LBooleanFormula (GhcPass p')]
forall a b. (a -> b) -> [a] -> [b]
map ((BooleanFormula (GhcPass p) -> BooleanFormula (GhcPass p'))
-> GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p))
-> GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p'))
forall a b.
(a -> b) -> GenLocated SrcSpanAnnL a -> GenLocated SrcSpanAnnL b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap BooleanFormula (GhcPass p) -> BooleanFormula (GhcPass p')
go) [LBooleanFormula (GhcPass p)]
[GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p))]
bfs
    go (Or     [LBooleanFormula (GhcPass p)]
bfs) = [LBooleanFormula (GhcPass p')] -> BooleanFormula (GhcPass p')
forall p. [LBooleanFormula p] -> BooleanFormula p
Or      ([LBooleanFormula (GhcPass p')] -> BooleanFormula (GhcPass p'))
-> [LBooleanFormula (GhcPass p')] -> BooleanFormula (GhcPass p')
forall a b. (a -> b) -> a -> b
$ (GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p))
 -> LBooleanFormula (GhcPass p'))
-> [GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p))]
-> [LBooleanFormula (GhcPass p')]
forall a b. (a -> b) -> [a] -> [b]
map ((BooleanFormula (GhcPass p) -> BooleanFormula (GhcPass p'))
-> GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p))
-> GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p'))
forall a b.
(a -> b) -> GenLocated SrcSpanAnnL a -> GenLocated SrcSpanAnnL b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap BooleanFormula (GhcPass p) -> BooleanFormula (GhcPass p')
go) [LBooleanFormula (GhcPass p)]
[GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p))]
bfs
    go (Parens LBooleanFormula (GhcPass p)
bf ) = LBooleanFormula (GhcPass p') -> BooleanFormula (GhcPass p')
forall p. LBooleanFormula p -> BooleanFormula p
Parens  (LBooleanFormula (GhcPass p') -> BooleanFormula (GhcPass p'))
-> LBooleanFormula (GhcPass p') -> BooleanFormula (GhcPass p')
forall a b. (a -> b) -> a -> b
$ (BooleanFormula (GhcPass p) -> BooleanFormula (GhcPass p'))
-> GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p))
-> GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p'))
forall a b.
(a -> b) -> GenLocated SrcSpanAnnL a -> GenLocated SrcSpanAnnL b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap BooleanFormula (GhcPass p) -> BooleanFormula (GhcPass p')
go LBooleanFormula (GhcPass p)
GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p))
bf

bfTraverse  :: Applicative f
            => (LIdP (GhcPass p) -> f (LIdP (GhcPass p')))
            -> BooleanFormula (GhcPass p)
            -> f (BooleanFormula (GhcPass p'))
bfTraverse :: forall (f :: * -> *) (p :: Pass) (p' :: Pass).
Applicative f =>
(LIdP (GhcPass p) -> f (LIdP (GhcPass p')))
-> BooleanFormula (GhcPass p) -> f (BooleanFormula (GhcPass p'))
bfTraverse LIdP (GhcPass p) -> f (LIdP (GhcPass p'))
f = BooleanFormula (GhcPass p) -> f (BooleanFormula (GhcPass p'))
go
  where
    go :: BooleanFormula (GhcPass p) -> f (BooleanFormula (GhcPass p'))
go (Var    LIdP (GhcPass p)
a  ) = LIdP (GhcPass p') -> BooleanFormula (GhcPass p')
XRecGhc (IdGhcP p') -> BooleanFormula (GhcPass p')
forall p. LIdP p -> BooleanFormula p
Var    (XRecGhc (IdGhcP p') -> BooleanFormula (GhcPass p'))
-> f (XRecGhc (IdGhcP p')) -> f (BooleanFormula (GhcPass p'))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> LIdP (GhcPass p) -> f (LIdP (GhcPass p'))
f LIdP (GhcPass p)
a
    go (And    [LBooleanFormula (GhcPass p)]
bfs) = [LBooleanFormula (GhcPass p')] -> BooleanFormula (GhcPass p')
[GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p'))]
-> BooleanFormula (GhcPass p')
forall p. [LBooleanFormula p] -> BooleanFormula p
And    ([GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p'))]
 -> BooleanFormula (GhcPass p'))
-> f [GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p'))]
-> f (BooleanFormula (GhcPass p'))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse @[] ((BooleanFormula (GhcPass p) -> f (BooleanFormula (GhcPass p')))
-> GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p))
-> f (GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p')))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b)
-> GenLocated SrcSpanAnnL a -> f (GenLocated SrcSpanAnnL b)
traverse BooleanFormula (GhcPass p) -> f (BooleanFormula (GhcPass p'))
go) [LBooleanFormula (GhcPass p)]
[GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p))]
bfs
    go (Or     [LBooleanFormula (GhcPass p)]
bfs) = [LBooleanFormula (GhcPass p')] -> BooleanFormula (GhcPass p')
[GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p'))]
-> BooleanFormula (GhcPass p')
forall p. [LBooleanFormula p] -> BooleanFormula p
Or     ([GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p'))]
 -> BooleanFormula (GhcPass p'))
-> f [GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p'))]
-> f (BooleanFormula (GhcPass p'))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse @[] ((BooleanFormula (GhcPass p) -> f (BooleanFormula (GhcPass p')))
-> GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p))
-> f (GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p')))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b)
-> GenLocated SrcSpanAnnL a -> f (GenLocated SrcSpanAnnL b)
traverse BooleanFormula (GhcPass p) -> f (BooleanFormula (GhcPass p'))
go) [LBooleanFormula (GhcPass p)]
[GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p))]
bfs
    go (Parens LBooleanFormula (GhcPass p)
bf ) = LBooleanFormula (GhcPass p') -> BooleanFormula (GhcPass p')
GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p'))
-> BooleanFormula (GhcPass p')
forall p. LBooleanFormula p -> BooleanFormula p
Parens (GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p'))
 -> BooleanFormula (GhcPass p'))
-> f (GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p')))
-> f (BooleanFormula (GhcPass p'))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (BooleanFormula (GhcPass p) -> f (BooleanFormula (GhcPass p')))
-> GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p))
-> f (GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p')))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b)
-> GenLocated SrcSpanAnnL a -> f (GenLocated SrcSpanAnnL b)
traverse BooleanFormula (GhcPass p) -> f (BooleanFormula (GhcPass p'))
go LBooleanFormula (GhcPass p)
GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p))
bf



{-
Note [Simplification of BooleanFormulas]
~~~~~~~~~~~~~~~~~~~~~~
The smart constructors (`mkAnd` and `mkOr`) do some attempt to simplify expressions. In particular,
 1. Collapsing nested ands and ors, so
     `(mkAnd [x, And [y,z]]`
    is represented as
     `And [x,y,z]`
    Implemented by `fromAnd`/`fromOr`
 2. Collapsing trivial ands and ors, so
     `mkAnd [x]` becomes just `x`.
    Implemented by mkAnd' / mkOr'
 3. Conjunction with false, disjunction with true is simplified, i.e.
     `mkAnd [mkFalse,x]` becomes `mkFalse`.
 4. Common subexpression elimination:
     `mkAnd [x,x,y]` is reduced to just `mkAnd [x,y]`.

This simplification is not exhaustive, in the sense that it will not produce
the smallest possible equivalent expression. For example,
`Or [And [x,y], And [x]]` could be simplified to `And [x]`, but it currently
is not. A general simplifier would need to use something like BDDs.

The reason behind the (crude) simplifier is to make for more user friendly
error messages. E.g. for the code
  > class Foo a where
  >     {-# MINIMAL bar, (foo, baq | foo, quux) #-}
  > instance Foo Int where
  >     bar = ...
  >     baz = ...
  >     quux = ...
We don't show a ridiculous error message like
    Implement () and (either (`foo' and ()) or (`foo' and ()))
-}

----------------------------------------------------------------------
-- Evaluation and simplification
----------------------------------------------------------------------

isFalse :: BooleanFormula (GhcPass p) -> Bool
isFalse :: forall (p :: Pass). BooleanFormula (GhcPass p) -> Bool
isFalse (Or []) = Bool
True
isFalse BooleanFormula (GhcPass p)
_ = Bool
False

isTrue :: BooleanFormula (GhcPass p) -> Bool
isTrue :: forall (p :: Pass). BooleanFormula (GhcPass p) -> Bool
isTrue (And []) = Bool
True
isTrue BooleanFormula (GhcPass p)
_ = Bool
False

eval :: (LIdP (GhcPass p) -> Bool) -> BooleanFormula (GhcPass p) -> Bool
eval :: forall (p :: Pass).
(LIdP (GhcPass p) -> Bool) -> BooleanFormula (GhcPass p) -> Bool
eval LIdP (GhcPass p) -> Bool
f (Var LIdP (GhcPass p)
x)  = LIdP (GhcPass p) -> Bool
f LIdP (GhcPass p)
x
eval LIdP (GhcPass p) -> Bool
f (And [LBooleanFormula (GhcPass p)]
xs) = (GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p)) -> Bool)
-> [GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p))] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((LIdP (GhcPass p) -> Bool) -> BooleanFormula (GhcPass p) -> Bool
forall (p :: Pass).
(LIdP (GhcPass p) -> Bool) -> BooleanFormula (GhcPass p) -> Bool
eval LIdP (GhcPass p) -> Bool
f (BooleanFormula (GhcPass p) -> Bool)
-> (GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p))
    -> BooleanFormula (GhcPass p))
-> GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p))
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p))
-> BooleanFormula (GhcPass p)
forall l e. GenLocated l e -> e
unLoc) [LBooleanFormula (GhcPass p)]
[GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p))]
xs
eval LIdP (GhcPass p) -> Bool
f (Or [LBooleanFormula (GhcPass p)]
xs)  = (GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p)) -> Bool)
-> [GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p))] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ((LIdP (GhcPass p) -> Bool) -> BooleanFormula (GhcPass p) -> Bool
forall (p :: Pass).
(LIdP (GhcPass p) -> Bool) -> BooleanFormula (GhcPass p) -> Bool
eval LIdP (GhcPass p) -> Bool
f (BooleanFormula (GhcPass p) -> Bool)
-> (GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p))
    -> BooleanFormula (GhcPass p))
-> GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p))
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p))
-> BooleanFormula (GhcPass p)
forall l e. GenLocated l e -> e
unLoc) [LBooleanFormula (GhcPass p)]
[GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p))]
xs
eval LIdP (GhcPass p) -> Bool
f (Parens LBooleanFormula (GhcPass p)
x) = (LIdP (GhcPass p) -> Bool) -> BooleanFormula (GhcPass p) -> Bool
forall (p :: Pass).
(LIdP (GhcPass p) -> Bool) -> BooleanFormula (GhcPass p) -> Bool
eval LIdP (GhcPass p) -> Bool
f (GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p))
-> BooleanFormula (GhcPass p)
forall l e. GenLocated l e -> e
unLoc LBooleanFormula (GhcPass p)
GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p))
x)

-- Simplify a boolean formula.
-- The argument function should give the truth of the atoms, or Nothing if undecided.
simplify :: forall p. Eq (LIdP (GhcPass p))
          => (LIdP (GhcPass p) ->  Maybe Bool)
          -> BooleanFormula (GhcPass p)
          -> BooleanFormula (GhcPass p)
simplify :: forall (p :: Pass).
Eq (LIdP (GhcPass p)) =>
(LIdP (GhcPass p) -> Maybe Bool)
-> BooleanFormula (GhcPass p) -> BooleanFormula (GhcPass p)
simplify LIdP (GhcPass p) -> Maybe Bool
f (Var LIdP (GhcPass p)
a) = case LIdP (GhcPass p) -> Maybe Bool
f LIdP (GhcPass p)
a of
  Maybe Bool
Nothing -> LIdP (GhcPass p) -> BooleanFormula (GhcPass p)
forall p. LIdP p -> BooleanFormula p
Var LIdP (GhcPass p)
a
  Just Bool
b  -> Bool -> BooleanFormula (GhcPass p)
forall p. Bool -> BooleanFormula p
mkBool Bool
b
simplify LIdP (GhcPass p) -> Maybe Bool
f (And [LBooleanFormula (GhcPass p)]
xs) = [LBooleanFormula (GhcPass p)] -> BooleanFormula (GhcPass p)
forall p.
(UnXRec p, Eq (LIdP p), Eq (LBooleanFormula p)) =>
[LBooleanFormula p] -> BooleanFormula p
mkAnd ((GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p))
 -> GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p)))
-> [GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p))]
-> [GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p))]
forall a b. (a -> b) -> [a] -> [b]
map ((BooleanFormula (GhcPass p) -> BooleanFormula (GhcPass p))
-> GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p))
-> GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p))
forall a b.
(a -> b) -> GenLocated SrcSpanAnnL a -> GenLocated SrcSpanAnnL b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((LIdP (GhcPass p) -> Maybe Bool)
-> BooleanFormula (GhcPass p) -> BooleanFormula (GhcPass p)
forall (p :: Pass).
Eq (LIdP (GhcPass p)) =>
(LIdP (GhcPass p) -> Maybe Bool)
-> BooleanFormula (GhcPass p) -> BooleanFormula (GhcPass p)
simplify LIdP (GhcPass p) -> Maybe Bool
f)) [LBooleanFormula (GhcPass p)]
[GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p))]
xs)
simplify LIdP (GhcPass p) -> Maybe Bool
f (Or [LBooleanFormula (GhcPass p)]
xs)  = [LBooleanFormula (GhcPass p)] -> BooleanFormula (GhcPass p)
forall p.
(UnXRec p, Eq (LIdP p), Eq (LBooleanFormula p)) =>
[LBooleanFormula p] -> BooleanFormula p
mkOr  ((GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p))
 -> GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p)))
-> [GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p))]
-> [GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p))]
forall a b. (a -> b) -> [a] -> [b]
map ((BooleanFormula (GhcPass p) -> BooleanFormula (GhcPass p))
-> GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p))
-> GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p))
forall a b.
(a -> b) -> GenLocated SrcSpanAnnL a -> GenLocated SrcSpanAnnL b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((LIdP (GhcPass p) -> Maybe Bool)
-> BooleanFormula (GhcPass p) -> BooleanFormula (GhcPass p)
forall (p :: Pass).
Eq (LIdP (GhcPass p)) =>
(LIdP (GhcPass p) -> Maybe Bool)
-> BooleanFormula (GhcPass p) -> BooleanFormula (GhcPass p)
simplify LIdP (GhcPass p) -> Maybe Bool
f)) [LBooleanFormula (GhcPass p)]
[GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p))]
xs)
simplify LIdP (GhcPass p) -> Maybe Bool
f (Parens LBooleanFormula (GhcPass p)
x) = (LIdP (GhcPass p) -> Maybe Bool)
-> BooleanFormula (GhcPass p) -> BooleanFormula (GhcPass p)
forall (p :: Pass).
Eq (LIdP (GhcPass p)) =>
(LIdP (GhcPass p) -> Maybe Bool)
-> BooleanFormula (GhcPass p) -> BooleanFormula (GhcPass p)
simplify LIdP (GhcPass p) -> Maybe Bool
f (GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p))
-> BooleanFormula (GhcPass p)
forall l e. GenLocated l e -> e
unLoc LBooleanFormula (GhcPass p)
GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p))
x)

-- Test if a boolean formula is satisfied when the given values are assigned to the atoms
-- if it is, returns Nothing
-- if it is not, return (Just remainder)
isUnsatisfied :: Eq (LIdP (GhcPass p))
              => (LIdP (GhcPass p) -> Bool)
              -> BooleanFormula (GhcPass p)
              -> Maybe (BooleanFormula (GhcPass p))
isUnsatisfied :: forall (p :: Pass).
Eq (LIdP (GhcPass p)) =>
(LIdP (GhcPass p) -> Bool)
-> BooleanFormula (GhcPass p) -> Maybe (BooleanFormula (GhcPass p))
isUnsatisfied LIdP (GhcPass p) -> Bool
f BooleanFormula (GhcPass p)
bf
    | BooleanFormula (GhcPass p) -> Bool
forall (p :: Pass). BooleanFormula (GhcPass p) -> Bool
isTrue BooleanFormula (GhcPass p)
bf' = Maybe (BooleanFormula (GhcPass p))
forall a. Maybe a
Nothing
    | Bool
otherwise  = BooleanFormula (GhcPass p) -> Maybe (BooleanFormula (GhcPass p))
forall a. a -> Maybe a
Just BooleanFormula (GhcPass p)
bf'
  where
  f' :: GenLocated (Anno (IdGhcP p)) (IdGhcP p) -> Maybe Bool
f' GenLocated (Anno (IdGhcP p)) (IdGhcP p)
x = if LIdP (GhcPass p) -> Bool
f LIdP (GhcPass p)
GenLocated (Anno (IdGhcP p)) (IdGhcP p)
x then Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True else Maybe Bool
forall a. Maybe a
Nothing
  bf' :: BooleanFormula (GhcPass p)
bf' = (LIdP (GhcPass p) -> Maybe Bool)
-> BooleanFormula (GhcPass p) -> BooleanFormula (GhcPass p)
forall (p :: Pass).
Eq (LIdP (GhcPass p)) =>
(LIdP (GhcPass p) -> Maybe Bool)
-> BooleanFormula (GhcPass p) -> BooleanFormula (GhcPass p)
simplify LIdP (GhcPass p) -> Maybe Bool
GenLocated (Anno (IdGhcP p)) (IdGhcP p) -> Maybe Bool
f' BooleanFormula (GhcPass p)
bf

-- prop_simplify:
--   eval f x == True   <==>  isTrue  (simplify (Just . f) x)
--   eval f x == False  <==>  isFalse (simplify (Just . f) x)

-- If the boolean formula holds, does that mean that the given atom is always true?
impliesAtom :: Eq (IdP (GhcPass p)) => BooleanFormula (GhcPass p) -> LIdP (GhcPass p) -> Bool
Var LIdP (GhcPass p)
x  impliesAtom :: forall (p :: Pass).
Eq (IdP (GhcPass p)) =>
BooleanFormula (GhcPass p) -> LIdP (GhcPass p) -> Bool
`impliesAtom` LIdP (GhcPass p)
y = (GenLocated (Anno (IdGhcP p)) (IdGhcP p) -> IdGhcP p
forall l e. GenLocated l e -> e
unLoc LIdP (GhcPass p)
GenLocated (Anno (IdGhcP p)) (IdGhcP p)
x) IdGhcP p -> IdGhcP p -> Bool
forall a. Eq a => a -> a -> Bool
== (GenLocated (Anno (IdGhcP p)) (IdGhcP p) -> IdGhcP p
forall l e. GenLocated l e -> e
unLoc LIdP (GhcPass p)
GenLocated (Anno (IdGhcP p)) (IdGhcP p)
y)
And [LBooleanFormula (GhcPass p)]
xs `impliesAtom` LIdP (GhcPass p)
y = (GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p)) -> Bool)
-> [GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p))] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p))
x -> GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p))
-> BooleanFormula (GhcPass p)
forall l e. GenLocated l e -> e
unLoc GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p))
x BooleanFormula (GhcPass p) -> LIdP (GhcPass p) -> Bool
forall (p :: Pass).
Eq (IdP (GhcPass p)) =>
BooleanFormula (GhcPass p) -> LIdP (GhcPass p) -> Bool
`impliesAtom` LIdP (GhcPass p)
y) [LBooleanFormula (GhcPass p)]
[GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p))]
xs
           -- we have all of xs, so one of them implying y is enough
Or  [LBooleanFormula (GhcPass p)]
xs `impliesAtom` LIdP (GhcPass p)
y = (GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p)) -> Bool)
-> [GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p))] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p))
x -> GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p))
-> BooleanFormula (GhcPass p)
forall l e. GenLocated l e -> e
unLoc GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p))
x BooleanFormula (GhcPass p) -> LIdP (GhcPass p) -> Bool
forall (p :: Pass).
Eq (IdP (GhcPass p)) =>
BooleanFormula (GhcPass p) -> LIdP (GhcPass p) -> Bool
`impliesAtom` LIdP (GhcPass p)
y) [LBooleanFormula (GhcPass p)]
[GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p))]
xs
Parens LBooleanFormula (GhcPass p)
x `impliesAtom` LIdP (GhcPass p)
y = GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p))
-> BooleanFormula (GhcPass p)
forall l e. GenLocated l e -> e
unLoc LBooleanFormula (GhcPass p)
GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p))
x BooleanFormula (GhcPass p) -> LIdP (GhcPass p) -> Bool
forall (p :: Pass).
Eq (IdP (GhcPass p)) =>
BooleanFormula (GhcPass p) -> LIdP (GhcPass p) -> Bool
`impliesAtom` LIdP (GhcPass p)
y

implies :: (Uniquable (IdP (GhcPass p))) => BooleanFormula (GhcPass p) -> BooleanFormula (GhcPass p) -> Bool
implies :: forall (p :: Pass).
Uniquable (IdP (GhcPass p)) =>
BooleanFormula (GhcPass p) -> BooleanFormula (GhcPass p) -> Bool
implies BooleanFormula (GhcPass p)
e1 BooleanFormula (GhcPass p)
e2 = Clause (GhcPass p) -> Clause (GhcPass p) -> Bool
forall (p :: Pass).
Uniquable (IdP (GhcPass p)) =>
Clause (GhcPass p) -> Clause (GhcPass p) -> Bool
go (UniqSet (IdP (GhcPass p))
-> [BooleanFormula (GhcPass p)] -> Clause (GhcPass p)
forall p. UniqSet (IdP p) -> [BooleanFormula p] -> Clause p
Clause UniqSet (IdP (GhcPass p))
UniqSet (IdGhcP p)
forall a. UniqSet a
emptyUniqSet [BooleanFormula (GhcPass p)
e1]) (UniqSet (IdP (GhcPass p))
-> [BooleanFormula (GhcPass p)] -> Clause (GhcPass p)
forall p. UniqSet (IdP p) -> [BooleanFormula p] -> Clause p
Clause UniqSet (IdP (GhcPass p))
UniqSet (IdGhcP p)
forall a. UniqSet a
emptyUniqSet [BooleanFormula (GhcPass p)
e2])
  where
    go :: Uniquable (IdP (GhcPass p)) => Clause (GhcPass p) -> Clause (GhcPass p) -> Bool
    go :: forall (p :: Pass).
Uniquable (IdP (GhcPass p)) =>
Clause (GhcPass p) -> Clause (GhcPass p) -> Bool
go l :: Clause (GhcPass p)
l@Clause{ clauseExprs :: forall p. Clause p -> [BooleanFormula p]
clauseExprs = BooleanFormula (GhcPass p)
hyp:[BooleanFormula (GhcPass p)]
hyps } Clause (GhcPass p)
r =
        case BooleanFormula (GhcPass p)
hyp of
            Var LIdP (GhcPass p)
x | IdP (GhcPass p) -> Clause (GhcPass p) -> Bool
forall p. Uniquable (IdP p) => IdP p -> Clause p -> Bool
memberClauseAtoms (GenLocated (Anno (IdGhcP p)) (IdGhcP p) -> IdGhcP p
forall l e. GenLocated l e -> e
unLoc LIdP (GhcPass p)
GenLocated (Anno (IdGhcP p)) (IdGhcP p)
x) Clause (GhcPass p)
r -> Bool
True
                  | Bool
otherwise -> Clause (GhcPass p) -> Clause (GhcPass p) -> Bool
forall (p :: Pass).
Uniquable (IdP (GhcPass p)) =>
Clause (GhcPass p) -> Clause (GhcPass p) -> Bool
go (Clause (GhcPass p) -> IdP (GhcPass p) -> Clause (GhcPass p)
forall p. Uniquable (IdP p) => Clause p -> IdP p -> Clause p
extendClauseAtoms Clause (GhcPass p)
l (GenLocated (Anno (IdGhcP p)) (IdGhcP p) -> IdGhcP p
forall l e. GenLocated l e -> e
unLoc LIdP (GhcPass p)
GenLocated (Anno (IdGhcP p)) (IdGhcP p)
x)) { clauseExprs = hyps } Clause (GhcPass p)
r
            Parens LBooleanFormula (GhcPass p)
hyp' -> Clause (GhcPass p) -> Clause (GhcPass p) -> Bool
forall (p :: Pass).
Uniquable (IdP (GhcPass p)) =>
Clause (GhcPass p) -> Clause (GhcPass p) -> Bool
go Clause (GhcPass p)
l { clauseExprs = unLoc hyp':hyps }     Clause (GhcPass p)
r
            And [LBooleanFormula (GhcPass p)]
hyps'  -> Clause (GhcPass p) -> Clause (GhcPass p) -> Bool
forall (p :: Pass).
Uniquable (IdP (GhcPass p)) =>
Clause (GhcPass p) -> Clause (GhcPass p) -> Bool
go Clause (GhcPass p)
l { clauseExprs = map unLoc hyps' ++ hyps } Clause (GhcPass p)
r
            Or [LBooleanFormula (GhcPass p)]
hyps'   -> (GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p)) -> Bool)
-> [GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p))] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p))
hyp' -> Clause (GhcPass p) -> Clause (GhcPass p) -> Bool
forall (p :: Pass).
Uniquable (IdP (GhcPass p)) =>
Clause (GhcPass p) -> Clause (GhcPass p) -> Bool
go Clause (GhcPass p)
l { clauseExprs = unLoc hyp':hyps } Clause (GhcPass p)
r) [LBooleanFormula (GhcPass p)]
[GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p))]
hyps'
    go Clause (GhcPass p)
l r :: Clause (GhcPass p)
r@Clause{ clauseExprs :: forall p. Clause p -> [BooleanFormula p]
clauseExprs = BooleanFormula (GhcPass p)
con:[BooleanFormula (GhcPass p)]
cons } =
        case BooleanFormula (GhcPass p)
con of
            Var LIdP (GhcPass p)
x | IdP (GhcPass p) -> Clause (GhcPass p) -> Bool
forall p. Uniquable (IdP p) => IdP p -> Clause p -> Bool
memberClauseAtoms (GenLocated (Anno (IdGhcP p)) (IdGhcP p) -> IdGhcP p
forall l e. GenLocated l e -> e
unLoc LIdP (GhcPass p)
GenLocated (Anno (IdGhcP p)) (IdGhcP p)
x) Clause (GhcPass p)
l -> Bool
True
                  | Bool
otherwise -> Clause (GhcPass p) -> Clause (GhcPass p) -> Bool
forall (p :: Pass).
Uniquable (IdP (GhcPass p)) =>
Clause (GhcPass p) -> Clause (GhcPass p) -> Bool
go Clause (GhcPass p)
l (Clause (GhcPass p) -> IdP (GhcPass p) -> Clause (GhcPass p)
forall p. Uniquable (IdP p) => Clause p -> IdP p -> Clause p
extendClauseAtoms Clause (GhcPass p)
r (GenLocated (Anno (IdGhcP p)) (IdGhcP p) -> IdGhcP p
forall l e. GenLocated l e -> e
unLoc LIdP (GhcPass p)
GenLocated (Anno (IdGhcP p)) (IdGhcP p)
x)) { clauseExprs = cons }
            Parens LBooleanFormula (GhcPass p)
con' -> Clause (GhcPass p) -> Clause (GhcPass p) -> Bool
forall (p :: Pass).
Uniquable (IdP (GhcPass p)) =>
Clause (GhcPass p) -> Clause (GhcPass p) -> Bool
go Clause (GhcPass p)
l Clause (GhcPass p)
r { clauseExprs = unLoc con':cons }
            And [LBooleanFormula (GhcPass p)]
cons'   -> (GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p)) -> Bool)
-> [GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p))] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p))
con' -> Clause (GhcPass p) -> Clause (GhcPass p) -> Bool
forall (p :: Pass).
Uniquable (IdP (GhcPass p)) =>
Clause (GhcPass p) -> Clause (GhcPass p) -> Bool
go Clause (GhcPass p)
l Clause (GhcPass p)
r { clauseExprs = unLoc con':cons }) [LBooleanFormula (GhcPass p)]
[GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p))]
cons'
            Or [LBooleanFormula (GhcPass p)]
cons'    -> Clause (GhcPass p) -> Clause (GhcPass p) -> Bool
forall (p :: Pass).
Uniquable (IdP (GhcPass p)) =>
Clause (GhcPass p) -> Clause (GhcPass p) -> Bool
go Clause (GhcPass p)
l Clause (GhcPass p)
r { clauseExprs = map unLoc cons' ++ cons }
    go Clause (GhcPass p)
_ Clause (GhcPass p)
_ = Bool
False

-- A small sequent calculus proof engine.
data Clause p = Clause {
        forall p. Clause p -> UniqSet (IdP p)
clauseAtoms :: UniqSet (IdP p),
        forall p. Clause p -> [BooleanFormula p]
clauseExprs :: [BooleanFormula p]
    }
extendClauseAtoms :: Uniquable (IdP p) => Clause p -> IdP p -> Clause p
extendClauseAtoms :: forall p. Uniquable (IdP p) => Clause p -> IdP p -> Clause p
extendClauseAtoms Clause p
c IdP p
x = Clause p
c { clauseAtoms = addOneToUniqSet (clauseAtoms c) x }

memberClauseAtoms :: Uniquable (IdP p) => IdP p -> Clause p -> Bool
memberClauseAtoms :: forall p. Uniquable (IdP p) => IdP p -> Clause p -> Bool
memberClauseAtoms IdP p
x Clause p
c = IdP p
x IdP p -> UniqSet (IdP p) -> Bool
forall a. Uniquable a => a -> UniqSet a -> Bool
`elementOfUniqSet` Clause p -> UniqSet (IdP p)
forall p. Clause p -> UniqSet (IdP p)
clauseAtoms Clause p
c

----------------------------------------------------------------------
-- Pretty printing
----------------------------------------------------------------------

-- Pretty print a BooleanFormula,
-- using the arguments as pretty printers for Var, And and Or respectively
pprBooleanFormula'  :: (Rational -> LIdP (GhcPass p) -> SDoc)
                    -> (Rational -> [SDoc] -> SDoc)
                    -> (Rational -> [SDoc] -> SDoc)
                    -> Rational -> BooleanFormula (GhcPass p) -> SDoc
pprBooleanFormula' :: forall (p :: Pass).
(Rational -> LIdP (GhcPass p) -> SDoc)
-> (Rational -> [SDoc] -> SDoc)
-> (Rational -> [SDoc] -> SDoc)
-> Rational
-> BooleanFormula (GhcPass p)
-> SDoc
pprBooleanFormula' Rational -> LIdP (GhcPass p) -> SDoc
pprVar Rational -> [SDoc] -> SDoc
pprAnd Rational -> [SDoc] -> SDoc
pprOr = Rational -> BooleanFormula (GhcPass p) -> SDoc
go
  where
  go :: Rational -> BooleanFormula (GhcPass p) -> SDoc
go Rational
p (Var LIdP (GhcPass p)
x)  = Rational -> LIdP (GhcPass p) -> SDoc
pprVar Rational
p LIdP (GhcPass p)
x
  go Rational
p (And []) = Bool -> SDoc -> SDoc
cparen (Rational
p Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
> Rational
0) SDoc
forall doc. IsOutput doc => doc
empty
  go Rational
p (And [LBooleanFormula (GhcPass p)]
xs) = Rational -> [SDoc] -> SDoc
pprAnd Rational
p ((GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p)) -> SDoc)
-> [GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p))] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map (Rational -> BooleanFormula (GhcPass p) -> SDoc
go Rational
3 (BooleanFormula (GhcPass p) -> SDoc)
-> (GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p))
    -> BooleanFormula (GhcPass p))
-> GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p))
-> SDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p))
-> BooleanFormula (GhcPass p)
forall l e. GenLocated l e -> e
unLoc) [LBooleanFormula (GhcPass p)]
[GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p))]
xs)
  go Rational
_ (Or  []) = SDoc -> SDoc
keyword (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"FALSE"
  go Rational
p (Or  [LBooleanFormula (GhcPass p)]
xs) = Rational -> [SDoc] -> SDoc
pprOr Rational
p ((GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p)) -> SDoc)
-> [GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p))] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map (Rational -> BooleanFormula (GhcPass p) -> SDoc
go Rational
2 (BooleanFormula (GhcPass p) -> SDoc)
-> (GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p))
    -> BooleanFormula (GhcPass p))
-> GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p))
-> SDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p))
-> BooleanFormula (GhcPass p)
forall l e. GenLocated l e -> e
unLoc) [LBooleanFormula (GhcPass p)]
[GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p))]
xs)
  go Rational
p (Parens LBooleanFormula (GhcPass p)
x) = Rational -> BooleanFormula (GhcPass p) -> SDoc
go Rational
p (GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p))
-> BooleanFormula (GhcPass p)
forall l e. GenLocated l e -> e
unLoc LBooleanFormula (GhcPass p)
GenLocated SrcSpanAnnL (BooleanFormula (GhcPass p))
x)

-- Pretty print in source syntax, "a | b | c,d,e"
pprBooleanFormula :: (Rational -> LIdP (GhcPass p) -> SDoc)
                  -> Rational -> BooleanFormula (GhcPass p) -> SDoc
pprBooleanFormula :: forall (p :: Pass).
(Rational -> LIdP (GhcPass p) -> SDoc)
-> Rational -> BooleanFormula (GhcPass p) -> SDoc
pprBooleanFormula Rational -> LIdP (GhcPass p) -> SDoc
pprVar = (Rational -> LIdP (GhcPass p) -> SDoc)
-> (Rational -> [SDoc] -> SDoc)
-> (Rational -> [SDoc] -> SDoc)
-> Rational
-> BooleanFormula (GhcPass p)
-> SDoc
forall (p :: Pass).
(Rational -> LIdP (GhcPass p) -> SDoc)
-> (Rational -> [SDoc] -> SDoc)
-> (Rational -> [SDoc] -> SDoc)
-> Rational
-> BooleanFormula (GhcPass p)
-> SDoc
pprBooleanFormula' Rational -> LIdP (GhcPass p) -> SDoc
pprVar Rational -> [SDoc] -> SDoc
forall {a}. (Ord a, Num a) => a -> [SDoc] -> SDoc
pprAnd Rational -> [SDoc] -> SDoc
forall {a}. (Ord a, Num a) => a -> [SDoc] -> SDoc
pprOr
  where
  pprAnd :: a -> [SDoc] -> SDoc
pprAnd a
p = Bool -> SDoc -> SDoc
cparen (a
p a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
3) (SDoc -> SDoc) -> ([SDoc] -> SDoc) -> [SDoc] -> SDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [SDoc] -> SDoc
forall doc. IsLine doc => [doc] -> doc
fsep ([SDoc] -> SDoc) -> ([SDoc] -> [SDoc]) -> [SDoc] -> SDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SDoc -> [SDoc] -> [SDoc]
forall doc. IsLine doc => doc -> [doc] -> [doc]
punctuate SDoc
forall doc. IsLine doc => doc
comma
  pprOr :: a -> [SDoc] -> SDoc
pprOr  a
p = Bool -> SDoc -> SDoc
cparen (a
p a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
2) (SDoc -> SDoc) -> ([SDoc] -> SDoc) -> [SDoc] -> SDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [SDoc] -> SDoc
forall doc. IsLine doc => [doc] -> doc
fsep ([SDoc] -> SDoc) -> ([SDoc] -> [SDoc]) -> [SDoc] -> SDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SDoc -> [SDoc] -> [SDoc]
forall a. a -> [a] -> [a]
intersperse SDoc
forall doc. IsLine doc => doc
vbar

-- Pretty print human in readable format, "either `a' or `b' or (`c', `d' and `e')"?
pprBooleanFormulaNice :: Outputable (LIdP (GhcPass p)) => BooleanFormula (GhcPass p) -> SDoc
pprBooleanFormulaNice :: forall (p :: Pass).
Outputable (LIdP (GhcPass p)) =>
BooleanFormula (GhcPass p) -> SDoc
pprBooleanFormulaNice = (Rational -> LIdP (GhcPass p) -> SDoc)
-> (Rational -> [SDoc] -> SDoc)
-> (Rational -> [SDoc] -> SDoc)
-> Rational
-> BooleanFormula (GhcPass p)
-> SDoc
forall (p :: Pass).
(Rational -> LIdP (GhcPass p) -> SDoc)
-> (Rational -> [SDoc] -> SDoc)
-> (Rational -> [SDoc] -> SDoc)
-> Rational
-> BooleanFormula (GhcPass p)
-> SDoc
pprBooleanFormula' Rational -> LIdP (GhcPass p) -> SDoc
Rational -> GenLocated (Anno (IdGhcP p)) (IdGhcP p) -> SDoc
forall {a} {p}. Outputable a => p -> a -> SDoc
pprVar Rational -> [SDoc] -> SDoc
forall {a}. (Ord a, Num a) => a -> [SDoc] -> SDoc
pprAnd Rational -> [SDoc] -> SDoc
forall {a}. (Ord a, Num a) => a -> [SDoc] -> SDoc
pprOr Rational
0
  where
  pprVar :: p -> a -> SDoc
pprVar p
_ = SDoc -> SDoc
quotes (SDoc -> SDoc) -> (a -> SDoc) -> a -> SDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> SDoc
forall a. Outputable a => a -> SDoc
ppr
  pprAnd :: a -> [SDoc] -> SDoc
pprAnd a
p = Bool -> SDoc -> SDoc
cparen (a
p a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
1) (SDoc -> SDoc) -> ([SDoc] -> SDoc) -> [SDoc] -> SDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [SDoc] -> SDoc
forall doc. IsLine doc => [doc] -> doc
pprAnd'
  pprAnd' :: [doc] -> doc
pprAnd' [] = doc
forall doc. IsOutput doc => doc
empty
  pprAnd' [doc
x,doc
y] = doc
x doc -> doc -> doc
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> doc
forall doc. IsLine doc => String -> doc
text String
"and" doc -> doc -> doc
forall doc. IsLine doc => doc -> doc -> doc
<+> doc
y
  pprAnd' (doc
x:[doc]
xs) = [doc] -> doc
forall doc. IsLine doc => [doc] -> doc
fsep (doc -> [doc] -> [doc]
forall doc. IsLine doc => doc -> [doc] -> [doc]
punctuate doc
forall doc. IsLine doc => doc
comma (NonEmpty doc -> [doc]
forall a. NonEmpty a -> [a]
init (doc
xdoc -> [doc] -> NonEmpty doc
forall a. a -> [a] -> NonEmpty a
:|[doc]
xs))) doc -> doc -> doc
forall doc. IsLine doc => doc -> doc -> doc
<> String -> doc
forall doc. IsLine doc => String -> doc
text String
", and" doc -> doc -> doc
forall doc. IsLine doc => doc -> doc -> doc
<+> NonEmpty doc -> doc
forall a. NonEmpty a -> a
last (doc
xdoc -> [doc] -> NonEmpty doc
forall a. a -> [a] -> NonEmpty a
:|[doc]
xs)
  pprOr :: a -> [SDoc] -> SDoc
pprOr a
p [SDoc]
xs = Bool -> SDoc -> SDoc
cparen (a
p a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
1) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"either" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [SDoc] -> SDoc
forall doc. IsLine doc => [doc] -> doc
sep (SDoc -> [SDoc] -> [SDoc]
forall a. a -> [a] -> [a]
intersperse (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"or") [SDoc]
xs)

instance OutputableBndrId p => Outputable (BooleanFormula (GhcPass p)) where
  ppr :: BooleanFormula (GhcPass p) -> SDoc
ppr = BooleanFormula (GhcPass p) -> SDoc
forall (p :: Pass).
OutputableBndrId p =>
BooleanFormula (GhcPass p) -> SDoc
pprBooleanFormulaNormal

pprBooleanFormulaNormal :: OutputableBndrId p => BooleanFormula (GhcPass p) -> SDoc
pprBooleanFormulaNormal :: forall (p :: Pass).
OutputableBndrId p =>
BooleanFormula (GhcPass p) -> SDoc
pprBooleanFormulaNormal = BooleanFormula (GhcPass p) -> SDoc
forall {p} {l} {l}.
(XRec p (IdP p) ~ GenLocated l (IdP p),
 XRec p (BooleanFormula p) ~ GenLocated l (BooleanFormula p),
 OutputableBndr (IdP p)) =>
BooleanFormula p -> SDoc
go
  where
    go :: BooleanFormula p -> SDoc
go (Var XRec p (IdP p)
x)    = IdP p -> SDoc
forall a. OutputableBndr a => a -> SDoc
pprPrefixOcc (GenLocated l (IdP p) -> IdP p
forall l e. GenLocated l e -> e
unLoc XRec p (IdP p)
GenLocated l (IdP p)
x)
    go (And [XRec p (BooleanFormula p)]
xs)   = [SDoc] -> SDoc
forall doc. IsLine doc => [doc] -> doc
fsep ([SDoc] -> SDoc) -> [SDoc] -> SDoc
forall a b. (a -> b) -> a -> b
$ SDoc -> [SDoc] -> [SDoc]
forall doc. IsLine doc => doc -> [doc] -> [doc]
punctuate SDoc
forall doc. IsLine doc => doc
comma ((GenLocated l (BooleanFormula p) -> SDoc)
-> [GenLocated l (BooleanFormula p)] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map (BooleanFormula p -> SDoc
go (BooleanFormula p -> SDoc)
-> (GenLocated l (BooleanFormula p) -> BooleanFormula p)
-> GenLocated l (BooleanFormula p)
-> SDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GenLocated l (BooleanFormula p) -> BooleanFormula p
forall l e. GenLocated l e -> e
unLoc) [XRec p (BooleanFormula p)]
[GenLocated l (BooleanFormula p)]
xs)
    go (Or [])    = SDoc -> SDoc
keyword (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"FALSE"
    go (Or [XRec p (BooleanFormula p)]
xs)    = [SDoc] -> SDoc
forall doc. IsLine doc => [doc] -> doc
fsep ([SDoc] -> SDoc) -> [SDoc] -> SDoc
forall a b. (a -> b) -> a -> b
$ SDoc -> [SDoc] -> [SDoc]
forall a. a -> [a] -> [a]
intersperse SDoc
forall doc. IsLine doc => doc
vbar ((GenLocated l (BooleanFormula p) -> SDoc)
-> [GenLocated l (BooleanFormula p)] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map (BooleanFormula p -> SDoc
go (BooleanFormula p -> SDoc)
-> (GenLocated l (BooleanFormula p) -> BooleanFormula p)
-> GenLocated l (BooleanFormula p)
-> SDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GenLocated l (BooleanFormula p) -> BooleanFormula p
forall l e. GenLocated l e -> e
unLoc) [XRec p (BooleanFormula p)]
[GenLocated l (BooleanFormula p)]
xs)
    go (Parens XRec p (BooleanFormula p)
x) = SDoc -> SDoc
forall doc. IsLine doc => doc -> doc
parens (BooleanFormula p -> SDoc
go (BooleanFormula p -> SDoc) -> BooleanFormula p -> SDoc
forall a b. (a -> b) -> a -> b
$ GenLocated l (BooleanFormula p) -> BooleanFormula p
forall l e. GenLocated l e -> e
unLoc XRec p (BooleanFormula p)
GenLocated l (BooleanFormula p)
x)