{-# LANGUAGE FlexibleContexts, ScopedTypeVariables, TypeFamilies, UndecidableInstances #-}
module Data.Logic.ATP.LitWrapper
    ( JL(unJL)
    ) where

import Data.Logic.ATP.Formulas
import Data.Logic.ATP.Lit
import Data.Logic.ATP.Pretty

-- | Wrapper type to make an IsLiteral value that happens to also be
-- JustLiteral.  The JL constructor is not exported, JL values can be
-- built using 'convertToLiteral'.
newtype JL a = JL {forall a. JL a -> a
unJL :: a}

instance Pretty a => Pretty (JL a) where
    pPrint :: JL a -> Doc
pPrint (JL a
x) = a -> Doc
forall a. Pretty a => a -> Doc
pPrint a
x

instance HasFixity a => HasFixity (JL a) where
    precedence :: JL a -> Precedence
precedence = a -> a
a -> Precedence
forall x. HasFixity x => x -> Precedence
precedence (a -> a) -> (JL a -> a) -> JL a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. JL a -> a
forall a. JL a -> a
unJL
    associativity :: JL a -> Associativity
associativity = a -> Associativity
forall x. HasFixity x => x -> Associativity
associativity (a -> Associativity) -> (JL a -> a) -> JL a -> Associativity
forall b c a. (b -> c) -> (a -> b) -> a -> c
. JL a -> a
forall a. JL a -> a
unJL

instance IsLiteral a => IsFormula (JL a) where
    type AtomOf (JL a) = AtomOf a
    asBool :: JL a -> Maybe Bool
asBool (JL a
x) = a -> Maybe Bool
forall formula. IsFormula formula => formula -> Maybe Bool
asBool a
x
    true :: JL a
true = a -> JL a
forall a. a -> JL a
JL (a
forall formula. IsFormula formula => formula
true :: a)
    false :: JL a
false = a -> JL a
forall a. a -> JL a
JL (a
forall formula. IsFormula formula => formula
false :: a)
    atomic :: AtomOf (JL a) -> JL a
atomic = a -> JL a
forall a. a -> JL a
JL (a -> JL a) -> (AtomOf a -> a) -> AtomOf a -> JL a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AtomOf a -> a
forall formula. IsFormula formula => AtomOf formula -> formula
atomic
    overatoms :: forall r. (AtomOf (JL a) -> r -> r) -> JL a -> r -> r
overatoms AtomOf (JL a) -> r -> r
f (JL a
x) r
r0 = (AtomOf a -> r -> r) -> a -> r -> r
forall lit r.
IsLiteral lit =>
(AtomOf lit -> r -> r) -> lit -> r -> r
overatomsLiteral' {-(\y r -> f (JL y) r)-} AtomOf a -> r -> r
AtomOf (JL a) -> r -> r
f a
x r
r0
    onatoms :: (AtomOf (JL a) -> AtomOf (JL a)) -> JL a -> JL a
onatoms AtomOf (JL a) -> AtomOf (JL a)
f (JL a
x) = a -> JL a
forall a. a -> JL a
JL ((AtomOf a -> AtomOf a) -> a -> a
forall formula.
IsFormula formula =>
(AtomOf formula -> AtomOf formula) -> formula -> formula
onatoms AtomOf a -> AtomOf a
AtomOf (JL a) -> AtomOf (JL a)
f a
x)

instance (IsFormula (JL a), IsLiteral a) => JustLiteral (JL a)

instance (IsFormula (JL a), IsLiteral a) => IsLiteral (JL a) where
    naiveNegate :: JL a -> JL a
naiveNegate (JL a
x) = a -> JL a
forall a. a -> JL a
JL (a -> a
forall lit. IsLiteral lit => lit -> lit
naiveNegate a
x)
    foldNegation :: forall r. (JL a -> r) -> (JL a -> r) -> JL a -> r
foldNegation JL a -> r
n JL a -> r
i (JL a
x) = (a -> r) -> (a -> r) -> a -> r
forall lit r. IsLiteral lit => (lit -> r) -> (lit -> r) -> lit -> r
forall r. (a -> r) -> (a -> r) -> a -> r
foldNegation (JL a -> r
n (JL a -> r) -> (a -> JL a) -> a -> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> JL a
forall a. a -> JL a
JL) (JL a -> r
i (JL a -> r) -> (a -> JL a) -> a -> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> JL a
forall a. a -> JL a
JL) a
x
    foldLiteral' :: forall r.
(JL a -> r)
-> (JL a -> r) -> (Bool -> r) -> (AtomOf (JL a) -> r) -> JL a -> r
foldLiteral' JL a -> r
ho JL a -> r
ne Bool -> r
tf AtomOf (JL a) -> r
at (JL a
x) = (a -> r) -> (a -> r) -> (Bool -> r) -> (AtomOf a -> r) -> a -> r
forall lit r.
IsLiteral lit =>
(lit -> r)
-> (lit -> r) -> (Bool -> r) -> (AtomOf lit -> r) -> lit -> r
forall r.
(a -> r) -> (a -> r) -> (Bool -> r) -> (AtomOf a -> r) -> a -> r
foldLiteral' (JL a -> r
ho (JL a -> r) -> (a -> JL a) -> a -> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> JL a
forall a. a -> JL a
JL) (JL a -> r
ne (JL a -> r) -> (a -> JL a) -> a -> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> JL a
forall a. a -> JL a
JL) Bool -> r
tf AtomOf a -> r
AtomOf (JL a) -> r
at a
x

-- | Unsafe local version of overatomsLiteral - assumes lit is a JustLiteral.
overatomsLiteral' :: IsLiteral lit => (AtomOf lit -> r -> r) -> lit -> r -> r
overatomsLiteral' :: forall lit r.
IsLiteral lit =>
(AtomOf lit -> r -> r) -> lit -> r -> r
overatomsLiteral' AtomOf lit -> r -> r
f lit
fm r
r0 =
        (lit -> r)
-> (lit -> r) -> (Bool -> r) -> (AtomOf lit -> r) -> lit -> r
forall lit r.
IsLiteral lit =>
(lit -> r)
-> (lit -> r) -> (Bool -> r) -> (AtomOf lit -> r) -> lit -> r
forall r.
(lit -> r)
-> (lit -> r) -> (Bool -> r) -> (AtomOf lit -> r) -> lit -> r
foldLiteral' lit -> r
forall a. HasCallStack => a
undefined lit -> r
ne (r -> Bool -> r
forall a b. a -> b -> a
const r
r0) ((AtomOf lit -> r -> r) -> r -> AtomOf lit -> r
forall a b c. (a -> b -> c) -> b -> a -> c
flip AtomOf lit -> r -> r
f r
r0) lit
fm
        where
          ne :: lit -> r
ne lit
fm' = (AtomOf lit -> r -> r) -> lit -> r -> r
forall lit r.
IsLiteral lit =>
(AtomOf lit -> r -> r) -> lit -> r -> r
overatomsLiteral' AtomOf lit -> r -> r
f lit
fm' r
r0