{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module      :  ./Propositional/Sublogic.hs
Description :  Sublogics for propositional logic
Copyright   :  (c) Dominik Luecke, Uni Bremen 2007
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  luecke@informatik.uni-bremen.de
Stability   :  experimental
Portability :  non-portable (imports Logic.Logic)

Sublogics for Propositional Logic
-}

{-
  Ref.

  http://en.wikipedia.org/wiki/Propositional_logic

  Till Mossakowski, Joseph Goguen, Razvan Diaconescu, Andrzej Tarlecki.
  What is a Logic?.
  In Jean-Yves Beziau (Ed.), Logica Universalis, pp. 113-@133. Birkhaeuser.
  2005.
-}

module Propositional.Sublogic
    (
     sl_basic_spec                  -- determine sublogic for basic spec
    , PropFormulae (..)             -- types of propositional formulae
    , PropSL (..)                   -- sublogics for propositional logic
    , sublogics_max                 -- join of sublogics
    , top                           -- Propositional
    , bottom                        -- Horn
    , sublogics_all                 -- all sublogics
    , sublogics_name                -- name of sublogics
    , sl_sig                        -- sublogic for a signature
    , sl_form                       -- sublogic for a formula
    , sl_sym                        -- sublogic for symbols
    , sl_symit                      -- sublogic for symbol items
    , sl_mor                        -- sublogic for morphisms
    , sl_symmap                     -- sublogic for symbol map items
    , prSymbolM                     -- projection of symbols
    , prSig                         -- projections of signatures
    , prMor                         -- projections of morphisms
    , prSymMapM                     -- projections of symbol maps
    , prSymM                        -- projections of SYMB_ITEMS
    , prFormulaM                    -- projections of formulae
    , prBasicSpec                   -- projections of basic specs
    , isProp
    , isHC
    )
    where

import Data.Data

import qualified Propositional.Tools as Tools
import qualified Propositional.AS_BASIC_Propositional as AS_BASIC

import qualified Propositional.Sign as Sign
import qualified Propositional.Symbol as Symbol
import qualified Propositional.Morphism as Morphism

import qualified Common.Lib.State as State
import qualified Common.AS_Annotation as AS_Anno

{- -----------------------------------------------------------------------------
datatypes                                                                 --
----------------------------------------------------------------------------- -}

-- | types of propositional formulae
data PropFormulae = PlainFormula      -- Formula without structural constraints
                  | HornClause        -- Horn Clause Formulae
                  deriving (Int -> PropFormulae -> ShowS
[PropFormulae] -> ShowS
PropFormulae -> String
(Int -> PropFormulae -> ShowS)
-> (PropFormulae -> String)
-> ([PropFormulae] -> ShowS)
-> Show PropFormulae
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [PropFormulae] -> ShowS
$cshowList :: [PropFormulae] -> ShowS
show :: PropFormulae -> String
$cshow :: PropFormulae -> String
showsPrec :: Int -> PropFormulae -> ShowS
$cshowsPrec :: Int -> PropFormulae -> ShowS
Show, PropFormulae -> PropFormulae -> Bool
(PropFormulae -> PropFormulae -> Bool)
-> (PropFormulae -> PropFormulae -> Bool) -> Eq PropFormulae
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: PropFormulae -> PropFormulae -> Bool
$c/= :: PropFormulae -> PropFormulae -> Bool
== :: PropFormulae -> PropFormulae -> Bool
$c== :: PropFormulae -> PropFormulae -> Bool
Eq, Eq PropFormulae
Eq PropFormulae =>
(PropFormulae -> PropFormulae -> Ordering)
-> (PropFormulae -> PropFormulae -> Bool)
-> (PropFormulae -> PropFormulae -> Bool)
-> (PropFormulae -> PropFormulae -> Bool)
-> (PropFormulae -> PropFormulae -> Bool)
-> (PropFormulae -> PropFormulae -> PropFormulae)
-> (PropFormulae -> PropFormulae -> PropFormulae)
-> Ord PropFormulae
PropFormulae -> PropFormulae -> Bool
PropFormulae -> PropFormulae -> Ordering
PropFormulae -> PropFormulae -> PropFormulae
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: PropFormulae -> PropFormulae -> PropFormulae
$cmin :: PropFormulae -> PropFormulae -> PropFormulae
max :: PropFormulae -> PropFormulae -> PropFormulae
$cmax :: PropFormulae -> PropFormulae -> PropFormulae
>= :: PropFormulae -> PropFormulae -> Bool
$c>= :: PropFormulae -> PropFormulae -> Bool
> :: PropFormulae -> PropFormulae -> Bool
$c> :: PropFormulae -> PropFormulae -> Bool
<= :: PropFormulae -> PropFormulae -> Bool
$c<= :: PropFormulae -> PropFormulae -> Bool
< :: PropFormulae -> PropFormulae -> Bool
$c< :: PropFormulae -> PropFormulae -> Bool
compare :: PropFormulae -> PropFormulae -> Ordering
$ccompare :: PropFormulae -> PropFormulae -> Ordering
$cp1Ord :: Eq PropFormulae
Ord, Typeable, Typeable PropFormulae
Constr
DataType
Typeable PropFormulae =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> PropFormulae -> c PropFormulae)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c PropFormulae)
-> (PropFormulae -> Constr)
-> (PropFormulae -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c PropFormulae))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c PropFormulae))
-> ((forall b. Data b => b -> b) -> PropFormulae -> PropFormulae)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> PropFormulae -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> PropFormulae -> r)
-> (forall u. (forall d. Data d => d -> u) -> PropFormulae -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> PropFormulae -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> PropFormulae -> m PropFormulae)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> PropFormulae -> m PropFormulae)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> PropFormulae -> m PropFormulae)
-> Data PropFormulae
PropFormulae -> Constr
PropFormulae -> DataType
(forall b. Data b => b -> b) -> PropFormulae -> PropFormulae
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PropFormulae -> c PropFormulae
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PropFormulae
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> PropFormulae -> u
forall u. (forall d. Data d => d -> u) -> PropFormulae -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PropFormulae -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PropFormulae -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> PropFormulae -> m PropFormulae
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PropFormulae -> m PropFormulae
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PropFormulae
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PropFormulae -> c PropFormulae
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c PropFormulae)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c PropFormulae)
$cHornClause :: Constr
$cPlainFormula :: Constr
$tPropFormulae :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> PropFormulae -> m PropFormulae
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PropFormulae -> m PropFormulae
gmapMp :: (forall d. Data d => d -> m d) -> PropFormulae -> m PropFormulae
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PropFormulae -> m PropFormulae
gmapM :: (forall d. Data d => d -> m d) -> PropFormulae -> m PropFormulae
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> PropFormulae -> m PropFormulae
gmapQi :: Int -> (forall d. Data d => d -> u) -> PropFormulae -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> PropFormulae -> u
gmapQ :: (forall d. Data d => d -> u) -> PropFormulae -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> PropFormulae -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PropFormulae -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PropFormulae -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PropFormulae -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PropFormulae -> r
gmapT :: (forall b. Data b => b -> b) -> PropFormulae -> PropFormulae
$cgmapT :: (forall b. Data b => b -> b) -> PropFormulae -> PropFormulae
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c PropFormulae)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c PropFormulae)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c PropFormulae)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c PropFormulae)
dataTypeOf :: PropFormulae -> DataType
$cdataTypeOf :: PropFormulae -> DataType
toConstr :: PropFormulae -> Constr
$ctoConstr :: PropFormulae -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PropFormulae
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PropFormulae
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PropFormulae -> c PropFormulae
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PropFormulae -> c PropFormulae
$cp1Data :: Typeable PropFormulae
Data)

-- | sublogics for propositional logic
data PropSL = PropSL
    {
      PropSL -> PropFormulae
format :: PropFormulae     -- Structural restrictions
    } deriving (Int -> PropSL -> ShowS
[PropSL] -> ShowS
PropSL -> String
(Int -> PropSL -> ShowS)
-> (PropSL -> String) -> ([PropSL] -> ShowS) -> Show PropSL
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [PropSL] -> ShowS
$cshowList :: [PropSL] -> ShowS
show :: PropSL -> String
$cshow :: PropSL -> String
showsPrec :: Int -> PropSL -> ShowS
$cshowsPrec :: Int -> PropSL -> ShowS
Show, PropSL -> PropSL -> Bool
(PropSL -> PropSL -> Bool)
-> (PropSL -> PropSL -> Bool) -> Eq PropSL
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: PropSL -> PropSL -> Bool
$c/= :: PropSL -> PropSL -> Bool
== :: PropSL -> PropSL -> Bool
$c== :: PropSL -> PropSL -> Bool
Eq, Eq PropSL
Eq PropSL =>
(PropSL -> PropSL -> Ordering)
-> (PropSL -> PropSL -> Bool)
-> (PropSL -> PropSL -> Bool)
-> (PropSL -> PropSL -> Bool)
-> (PropSL -> PropSL -> Bool)
-> (PropSL -> PropSL -> PropSL)
-> (PropSL -> PropSL -> PropSL)
-> Ord PropSL
PropSL -> PropSL -> Bool
PropSL -> PropSL -> Ordering
PropSL -> PropSL -> PropSL
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: PropSL -> PropSL -> PropSL
$cmin :: PropSL -> PropSL -> PropSL
max :: PropSL -> PropSL -> PropSL
$cmax :: PropSL -> PropSL -> PropSL
>= :: PropSL -> PropSL -> Bool
$c>= :: PropSL -> PropSL -> Bool
> :: PropSL -> PropSL -> Bool
$c> :: PropSL -> PropSL -> Bool
<= :: PropSL -> PropSL -> Bool
$c<= :: PropSL -> PropSL -> Bool
< :: PropSL -> PropSL -> Bool
$c< :: PropSL -> PropSL -> Bool
compare :: PropSL -> PropSL -> Ordering
$ccompare :: PropSL -> PropSL -> Ordering
$cp1Ord :: Eq PropSL
Ord, Typeable, Typeable PropSL
Constr
DataType
Typeable PropSL =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> PropSL -> c PropSL)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c PropSL)
-> (PropSL -> Constr)
-> (PropSL -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c PropSL))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PropSL))
-> ((forall b. Data b => b -> b) -> PropSL -> PropSL)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> PropSL -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> PropSL -> r)
-> (forall u. (forall d. Data d => d -> u) -> PropSL -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> PropSL -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> PropSL -> m PropSL)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> PropSL -> m PropSL)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> PropSL -> m PropSL)
-> Data PropSL
PropSL -> Constr
PropSL -> DataType
(forall b. Data b => b -> b) -> PropSL -> PropSL
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PropSL -> c PropSL
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PropSL
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> PropSL -> u
forall u. (forall d. Data d => d -> u) -> PropSL -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PropSL -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PropSL -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> PropSL -> m PropSL
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PropSL -> m PropSL
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PropSL
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PropSL -> c PropSL
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c PropSL)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PropSL)
$cPropSL :: Constr
$tPropSL :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> PropSL -> m PropSL
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PropSL -> m PropSL
gmapMp :: (forall d. Data d => d -> m d) -> PropSL -> m PropSL
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PropSL -> m PropSL
gmapM :: (forall d. Data d => d -> m d) -> PropSL -> m PropSL
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> PropSL -> m PropSL
gmapQi :: Int -> (forall d. Data d => d -> u) -> PropSL -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> PropSL -> u
gmapQ :: (forall d. Data d => d -> u) -> PropSL -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> PropSL -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PropSL -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PropSL -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PropSL -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PropSL -> r
gmapT :: (forall b. Data b => b -> b) -> PropSL -> PropSL
$cgmapT :: (forall b. Data b => b -> b) -> PropSL -> PropSL
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PropSL)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PropSL)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c PropSL)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c PropSL)
dataTypeOf :: PropSL -> DataType
$cdataTypeOf :: PropSL -> DataType
toConstr :: PropSL -> Constr
$ctoConstr :: PropSL -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PropSL
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PropSL
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PropSL -> c PropSL
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PropSL -> c PropSL
$cp1Data :: Typeable PropSL
Data)

isProp :: PropSL -> Bool
isProp :: PropSL -> Bool
isProp sl :: PropSL
sl = PropSL -> PropFormulae
format PropSL
sl PropFormulae -> PropFormulae -> Bool
forall a. Eq a => a -> a -> Bool
== PropFormulae
PlainFormula

isHC :: PropSL -> Bool
isHC :: PropSL -> Bool
isHC sl :: PropSL
sl = PropSL -> PropFormulae
format PropSL
sl PropFormulae -> PropFormulae -> Bool
forall a. Eq a => a -> a -> Bool
== PropFormulae
HornClause

-- | comparison of sublogics
compareLE :: PropSL -> PropSL -> Bool
compareLE :: PropSL -> PropSL -> Bool
compareLE p1 :: PropSL
p1 p2 :: PropSL
p2 =
    let f1 :: PropFormulae
f1 = PropSL -> PropFormulae
format PropSL
p1
        f2 :: PropFormulae
f2 = PropSL -> PropFormulae
format PropSL
p2
    in
      case (PropFormulae
f1, PropFormulae
f2) of
        (_, PlainFormula) -> Bool
True
        (HornClause, HornClause) -> Bool
True
        (_, HornClause) -> Bool
False

{- ----------------------------------------------------------------------------
Special elements in the Lattice of logics                                --
---------------------------------------------------------------------------- -}

top :: PropSL
top :: PropSL
top = PropFormulae -> PropSL
PropSL PropFormulae
PlainFormula

bottom :: PropSL
bottom :: PropSL
bottom = PropFormulae -> PropSL
PropSL PropFormulae
HornClause

need_PF :: PropSL
need_PF :: PropSL
need_PF = PropSL
bottom { format :: PropFormulae
format = PropFormulae
PlainFormula }

{- -----------------------------------------------------------------------------
join and max                                                              --
----------------------------------------------------------------------------- -}

sublogics_join :: (PropFormulae -> PropFormulae -> PropFormulae)
                  -> PropSL -> PropSL -> PropSL
sublogics_join :: (PropFormulae -> PropFormulae -> PropFormulae)
-> PropSL -> PropSL -> PropSL
sublogics_join pfF :: PropFormulae -> PropFormulae -> PropFormulae
pfF a :: PropSL
a b :: PropSL
b = PropSL :: PropFormulae -> PropSL
PropSL
                         {
                           format :: PropFormulae
format = PropFormulae -> PropFormulae -> PropFormulae
pfF (PropSL -> PropFormulae
format PropSL
a) (PropSL -> PropFormulae
format PropSL
b)
                         }

joinType :: PropFormulae -> PropFormulae -> PropFormulae
joinType :: PropFormulae -> PropFormulae -> PropFormulae
joinType HornClause HornClause = PropFormulae
HornClause
joinType _ _ = PropFormulae
PlainFormula

sublogics_max :: PropSL -> PropSL -> PropSL
sublogics_max :: PropSL -> PropSL -> PropSL
sublogics_max = (PropFormulae -> PropFormulae -> PropFormulae)
-> PropSL -> PropSL -> PropSL
sublogics_join PropFormulae -> PropFormulae -> PropFormulae
joinType

{- -----------------------------------------------------------------------------
Helpers                                                                   --
----------------------------------------------------------------------------- -}

-- compute sublogics from a list of sublogics
--
comp_list :: [PropSL] -> PropSL
comp_list :: [PropSL] -> PropSL
comp_list = (PropSL -> PropSL -> PropSL) -> PropSL -> [PropSL] -> PropSL
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl PropSL -> PropSL -> PropSL
sublogics_max PropSL
bottom

{- ----------------------------------------------------------------------------
Functions to compute minimal sublogic for a given element, these work    --
by recursing into all subelements                                        --
---------------------------------------------------------------------------- -}

-- | determines the sublogic for symbol map items
sl_symmap :: PropSL -> AS_BASIC.SYMB_MAP_ITEMS -> PropSL
sl_symmap :: PropSL -> SYMB_MAP_ITEMS -> PropSL
sl_symmap ps :: PropSL
ps _ = PropSL
ps

-- | determines the sublogic for a morphism
sl_mor :: PropSL -> Morphism.Morphism -> PropSL
sl_mor :: PropSL -> Morphism -> PropSL
sl_mor ps :: PropSL
ps _ = PropSL
ps

-- | determines the sublogic for a Signature
sl_sig :: PropSL -> Sign.Sign -> PropSL
sl_sig :: PropSL -> Sign -> PropSL
sl_sig ps :: PropSL
ps _ = PropSL
ps

-- | determines the sublogic for Symbol items
sl_symit :: PropSL -> AS_BASIC.SYMB_ITEMS -> PropSL
sl_symit :: PropSL -> SYMB_ITEMS -> PropSL
sl_symit ps :: PropSL
ps _ = PropSL
ps

-- | determines the sublogic for symbols
sl_sym :: PropSL -> Symbol.Symbol -> PropSL
sl_sym :: PropSL -> Symbol -> PropSL
sl_sym ps :: PropSL
ps _ = PropSL
ps

-- | determines sublogic for formula
sl_form :: PropSL -> AS_BASIC.FORMULA -> PropSL
sl_form :: PropSL -> FORMULA -> PropSL
sl_form ps :: PropSL
ps f :: FORMULA
f = PropSL -> [FORMULA] -> PropSL
sl_fl_form PropSL
ps ([FORMULA] -> PropSL) -> [FORMULA] -> PropSL
forall a b. (a -> b) -> a -> b
$ FORMULA -> [FORMULA]
Tools.flatten FORMULA
f

-- | determines sublogic for flattened formula
sl_fl_form :: PropSL -> [AS_BASIC.FORMULA] -> PropSL
sl_fl_form :: PropSL -> [FORMULA] -> PropSL
sl_fl_form ps :: PropSL
ps f :: [FORMULA]
f = (PropSL -> PropSL -> PropSL) -> PropSL -> [PropSL] -> PropSL
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl PropSL -> PropSL -> PropSL
sublogics_max PropSL
ps
  ([PropSL] -> PropSL) -> [PropSL] -> PropSL
forall a b. (a -> b) -> a -> b
$ (FORMULA -> PropSL) -> [FORMULA] -> [PropSL]
forall a b. (a -> b) -> [a] -> [b]
map (\ x :: FORMULA
x -> State Int PropSL -> Int -> PropSL
forall s a. State s a -> s -> a
State.evalState (PropSL -> FORMULA -> State Int PropSL
ana_form PropSL
ps FORMULA
x) 0) [FORMULA]
f

-- analysis of single "clauses"
ana_form :: PropSL -> AS_BASIC.FORMULA -> State.State Int PropSL
ana_form :: PropSL -> FORMULA -> State Int PropSL
ana_form ps :: PropSL
ps f :: FORMULA
f =
    case FORMULA
f of
      AS_BASIC.Conjunction l :: [FORMULA]
l _ ->
          do
            Int
st <- State Int Int
forall s. State s s
State.get
            PropSL -> State Int PropSL
forall (m :: * -> *) a. Monad m => a -> m a
return (PropSL -> State Int PropSL) -> PropSL -> State Int PropSL
forall a b. (a -> b) -> a -> b
$ PropSL -> PropSL -> PropSL
sublogics_max PropSL
need_PF (PropSL -> PropSL) -> PropSL -> PropSL
forall a b. (a -> b) -> a -> b
$ [PropSL] -> PropSL
comp_list ([PropSL] -> PropSL) -> [PropSL] -> PropSL
forall a b. (a -> b) -> a -> b
$ (FORMULA -> PropSL) -> [FORMULA] -> [PropSL]
forall a b. (a -> b) -> [a] -> [b]
map
              (\ x :: FORMULA
x -> State Int PropSL -> Int -> PropSL
forall s a. State s a -> s -> a
State.evalState (PropSL -> FORMULA -> State Int PropSL
ana_form PropSL
ps FORMULA
x) (Int
st Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1)) [FORMULA]
l
      AS_BASIC.Implication l :: FORMULA
l m :: FORMULA
m _ ->
          do
             Int
st <- State Int Int
forall s. State s s
State.get
             let analyze :: PropSL
analyze = PropSL -> PropSL -> PropSL
sublogics_max PropSL
need_PF (PropSL -> PropSL) -> PropSL -> PropSL
forall a b. (a -> b) -> a -> b
$ PropSL -> PropSL -> PropSL
sublogics_max
                   ((\ x :: FORMULA
x -> State Int PropSL -> Int -> PropSL
forall s a. State s a -> s -> a
State.evalState (PropSL -> FORMULA -> State Int PropSL
ana_form PropSL
ps FORMULA
x) (Int
st Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1)) FORMULA
l)
                   ((\ x :: FORMULA
x -> State Int PropSL -> Int -> PropSL
forall s a. State s a -> s -> a
State.evalState (PropSL -> FORMULA -> State Int PropSL
ana_form PropSL
ps FORMULA
x) (Int
st Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1)) FORMULA
m)
             PropSL -> State Int PropSL
forall (m :: * -> *) a. Monad m => a -> m a
return (PropSL -> State Int PropSL) -> PropSL -> State Int PropSL
forall a b. (a -> b) -> a -> b
$
                    if Int
st Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< 1 Bool -> Bool -> Bool
&& PropSL -> PropFormulae
format PropSL
ps PropFormulae -> PropFormulae -> Bool
forall a. Eq a => a -> a -> Bool
== PropFormulae
HornClause Bool -> Bool -> Bool
&& FORMULA -> FORMULA -> Bool
checkHornPos FORMULA
l FORMULA
m
                    then PropSL
ps else PropSL
analyze
      AS_BASIC.Equivalence l :: FORMULA
l m :: FORMULA
m _ ->
           do
             Int
st <- State Int Int
forall s. State s s
State.get
             PropSL -> State Int PropSL
forall (m :: * -> *) a. Monad m => a -> m a
return (PropSL -> State Int PropSL) -> PropSL -> State Int PropSL
forall a b. (a -> b) -> a -> b
$ PropSL -> PropSL -> PropSL
sublogics_max PropSL
need_PF (PropSL -> PropSL) -> PropSL -> PropSL
forall a b. (a -> b) -> a -> b
$ PropSL -> PropSL -> PropSL
sublogics_max
               ((\ x :: FORMULA
x -> State Int PropSL -> Int -> PropSL
forall s a. State s a -> s -> a
State.evalState (PropSL -> FORMULA -> State Int PropSL
ana_form PropSL
ps FORMULA
x) (Int
st Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1)) FORMULA
l)
               ((\ x :: FORMULA
x -> State Int PropSL -> Int -> PropSL
forall s a. State s a -> s -> a
State.evalState (PropSL -> FORMULA -> State Int PropSL
ana_form PropSL
ps FORMULA
x) (Int
st Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1)) FORMULA
m)
      AS_BASIC.Negation l :: FORMULA
l _ ->
          if FORMULA -> Bool
isLiteral FORMULA
l
          then PropSL -> State Int PropSL
forall (m :: * -> *) a. Monad m => a -> m a
return PropSL
ps
          else
              do
                Int
st <- State Int Int
forall s. State s s
State.get
                PropSL -> State Int PropSL
forall (m :: * -> *) a. Monad m => a -> m a
return (PropSL -> State Int PropSL) -> PropSL -> State Int PropSL
forall a b. (a -> b) -> a -> b
$ (\ x :: FORMULA
x -> State Int PropSL -> Int -> PropSL
forall s a. State s a -> s -> a
State.evalState (PropSL -> FORMULA -> State Int PropSL
ana_form PropSL
ps FORMULA
x) (Int
st Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1)) FORMULA
l
      AS_BASIC.Disjunction l :: [FORMULA]
l _ ->
                    let lprime :: [FORMULA]
lprime = (FORMULA -> [FORMULA]) -> [FORMULA] -> [FORMULA]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap FORMULA -> [FORMULA]
Tools.flattenDis [FORMULA]
l in
                    if (FORMULA -> Bool) -> [FORMULA] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all FORMULA -> Bool
isLiteral [FORMULA]
lprime
                    then PropSL -> State Int PropSL
forall (m :: * -> *) a. Monad m => a -> m a
return (PropSL -> State Int PropSL) -> PropSL -> State Int PropSL
forall a b. (a -> b) -> a -> b
$
                          if [FORMULA] -> Int -> Bool
moreThanNLit [FORMULA]
lprime 1
                          then PropSL -> PropSL -> PropSL
sublogics_max PropSL
need_PF PropSL
ps else PropSL
ps
                    else
                        do
                          Int
st <- State Int Int
forall s. State s s
State.get
                          PropSL -> State Int PropSL
forall (m :: * -> *) a. Monad m => a -> m a
return (PropSL -> State Int PropSL) -> PropSL -> State Int PropSL
forall a b. (a -> b) -> a -> b
$ PropSL -> PropSL -> PropSL
sublogics_max PropSL
need_PF (PropSL -> PropSL) -> PropSL -> PropSL
forall a b. (a -> b) -> a -> b
$ [PropSL] -> PropSL
comp_list ([PropSL] -> PropSL) -> [PropSL] -> PropSL
forall a b. (a -> b) -> a -> b
$ (FORMULA -> PropSL) -> [FORMULA] -> [PropSL]
forall a b. (a -> b) -> [a] -> [b]
map
                            (\ x :: FORMULA
x -> State Int PropSL -> Int -> PropSL
forall s a. State s a -> s -> a
State.evalState (PropSL -> FORMULA -> State Int PropSL
ana_form PropSL
ps FORMULA
x) (Int
st Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1))
                                      [FORMULA]
lprime
      AS_BASIC.True_atom _ -> PropSL -> State Int PropSL
forall (m :: * -> *) a. Monad m => a -> m a
return PropSL
ps
      AS_BASIC.False_atom _ -> PropSL -> State Int PropSL
forall (m :: * -> *) a. Monad m => a -> m a
return PropSL
ps
      AS_BASIC.Predication _ -> PropSL -> State Int PropSL
forall (m :: * -> *) a. Monad m => a -> m a
return PropSL
ps

moreThanNLit :: [AS_BASIC.FORMULA] -> Int -> Bool
moreThanNLit :: [FORMULA] -> Int -> Bool
moreThanNLit form :: [FORMULA]
form n :: Int
n = (Int -> Bool -> Int) -> Int -> [Bool] -> Int
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ y :: Int
y x :: Bool
x -> if Bool
x then Int
y Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1 else Int
y) 0
  ((FORMULA -> Bool) -> [FORMULA] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map FORMULA -> Bool
isPosLiteral [FORMULA]
form) Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
n

-- determines wheter a Formula is a literal
isLiteral :: AS_BASIC.FORMULA -> Bool
isLiteral :: FORMULA -> Bool
isLiteral (AS_BASIC.Predication _) = Bool
True
isLiteral (AS_BASIC.Negation (AS_BASIC.Predication _) _ ) = Bool
True
isLiteral (AS_BASIC.Negation _ _) = Bool
False
isLiteral (AS_BASIC.Conjunction _ _) = Bool
False
isLiteral (AS_BASIC.Implication {}) = Bool
False
isLiteral (AS_BASIC.Equivalence {}) = Bool
False
isLiteral (AS_BASIC.Disjunction _ _) = Bool
False
isLiteral (AS_BASIC.True_atom _ ) = Bool
True
isLiteral (AS_BASIC.False_atom _) = Bool
True

-- determines wheter a Formula is a positive literal
isPosLiteral :: AS_BASIC.FORMULA -> Bool
isPosLiteral :: FORMULA -> Bool
isPosLiteral (AS_BASIC.Predication _) = Bool
True
isPosLiteral (AS_BASIC.Negation _ _) = Bool
False
isPosLiteral (AS_BASIC.Conjunction _ _) = Bool
False
isPosLiteral (AS_BASIC.Implication {}) = Bool
False
isPosLiteral (AS_BASIC.Equivalence {}) = Bool
False
isPosLiteral (AS_BASIC.Disjunction _ _) = Bool
False
isPosLiteral (AS_BASIC.True_atom _ ) = Bool
True
isPosLiteral (AS_BASIC.False_atom _) = Bool
True

-- | determines subloig for basic items
sl_basic_items :: PropSL -> AS_BASIC.BASIC_ITEMS -> PropSL
sl_basic_items :: PropSL -> BASIC_ITEMS -> PropSL
sl_basic_items ps :: PropSL
ps bi :: BASIC_ITEMS
bi =
    case BASIC_ITEMS
bi of
      AS_BASIC.Pred_decl _ -> PropSL
ps
      AS_BASIC.Axiom_items xs :: [Annoted FORMULA]
xs -> [PropSL] -> PropSL
comp_list ([PropSL] -> PropSL) -> [PropSL] -> PropSL
forall a b. (a -> b) -> a -> b
$ (Annoted FORMULA -> PropSL) -> [Annoted FORMULA] -> [PropSL]
forall a b. (a -> b) -> [a] -> [b]
map (PropSL -> FORMULA -> PropSL
sl_form PropSL
ps (FORMULA -> PropSL)
-> (Annoted FORMULA -> FORMULA) -> Annoted FORMULA -> PropSL
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted FORMULA -> FORMULA
forall a. Annoted a -> a
AS_Anno.item) [Annoted FORMULA]
xs

-- | determines sublogic for basic spec
sl_basic_spec :: PropSL -> AS_BASIC.BASIC_SPEC -> PropSL
sl_basic_spec :: PropSL -> BASIC_SPEC -> PropSL
sl_basic_spec ps :: PropSL
ps (AS_BASIC.Basic_spec spec :: [Annoted BASIC_ITEMS]
spec) =
    [PropSL] -> PropSL
comp_list ([PropSL] -> PropSL) -> [PropSL] -> PropSL
forall a b. (a -> b) -> a -> b
$ (Annoted BASIC_ITEMS -> PropSL)
-> [Annoted BASIC_ITEMS] -> [PropSL]
forall a b. (a -> b) -> [a] -> [b]
map (PropSL -> BASIC_ITEMS -> PropSL
sl_basic_items PropSL
ps (BASIC_ITEMS -> PropSL)
-> (Annoted BASIC_ITEMS -> BASIC_ITEMS)
-> Annoted BASIC_ITEMS
-> PropSL
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted BASIC_ITEMS -> BASIC_ITEMS
forall a. Annoted a -> a
AS_Anno.item) [Annoted BASIC_ITEMS]
spec

-- | all sublogics
sublogics_all :: [PropSL]
sublogics_all :: [PropSL]
sublogics_all =
    [PropSL :: PropFormulae -> PropSL
PropSL
     {
       format :: PropFormulae
format = PropFormulae
HornClause
     }
    , PropSL :: PropFormulae -> PropSL
PropSL
     {
       format :: PropFormulae
format = PropFormulae
PlainFormula
     }
    ]

{- -----------------------------------------------------------------------------
Conversion functions to String                                            --
----------------------------------------------------------------------------- -}

sublogics_name :: PropSL -> String
sublogics_name :: PropSL -> String
sublogics_name f :: PropSL
f = case PropSL -> PropFormulae
format PropSL
f of
      HornClause -> "HornClause"
      PlainFormula -> "Prop"

{- -----------------------------------------------------------------------------
Projections to sublogics                                                  --
----------------------------------------------------------------------------- -}

prSymbolM :: PropSL -> Symbol.Symbol -> Maybe Symbol.Symbol
prSymbolM :: PropSL -> Symbol -> Maybe Symbol
prSymbolM _ = Symbol -> Maybe Symbol
forall a. a -> Maybe a
Just

prSig :: PropSL -> Sign.Sign -> Sign.Sign
prSig :: PropSL -> Sign -> Sign
prSig _ sig :: Sign
sig = Sign
sig

prMor :: PropSL -> Morphism.Morphism -> Morphism.Morphism
prMor :: PropSL -> Morphism -> Morphism
prMor _ mor :: Morphism
mor = Morphism
mor

prSymMapM :: PropSL
          -> AS_BASIC.SYMB_MAP_ITEMS
          -> Maybe AS_BASIC.SYMB_MAP_ITEMS
prSymMapM :: PropSL -> SYMB_MAP_ITEMS -> Maybe SYMB_MAP_ITEMS
prSymMapM _ = SYMB_MAP_ITEMS -> Maybe SYMB_MAP_ITEMS
forall a. a -> Maybe a
Just

prSymM :: PropSL -> AS_BASIC.SYMB_ITEMS -> Maybe AS_BASIC.SYMB_ITEMS
prSymM :: PropSL -> SYMB_ITEMS -> Maybe SYMB_ITEMS
prSymM _ = SYMB_ITEMS -> Maybe SYMB_ITEMS
forall a. a -> Maybe a
Just

-- keep an element if its computed sublogic is in the given sublogic
--

prFormulaM :: PropSL -> AS_BASIC.FORMULA -> Maybe AS_BASIC.FORMULA
prFormulaM :: PropSL -> FORMULA -> Maybe FORMULA
prFormulaM sl :: PropSL
sl form :: FORMULA
form
           | PropSL -> PropSL -> Bool
compareLE (PropSL -> FORMULA -> PropSL
sl_form PropSL
bottom FORMULA
form) PropSL
sl = FORMULA -> Maybe FORMULA
forall a. a -> Maybe a
Just FORMULA
form
           | Bool
otherwise = Maybe FORMULA
forall a. Maybe a
Nothing

prPredItem :: PropSL -> AS_BASIC.PRED_ITEM -> AS_BASIC.PRED_ITEM
prPredItem :: PropSL -> PRED_ITEM -> PRED_ITEM
prPredItem _ prI :: PRED_ITEM
prI = PRED_ITEM
prI

prBASIC_items :: PropSL -> AS_BASIC.BASIC_ITEMS -> AS_BASIC.BASIC_ITEMS
prBASIC_items :: PropSL -> BASIC_ITEMS -> BASIC_ITEMS
prBASIC_items pSL :: PropSL
pSL bI :: BASIC_ITEMS
bI =
    case BASIC_ITEMS
bI of
      AS_BASIC.Pred_decl pI :: PRED_ITEM
pI -> PRED_ITEM -> BASIC_ITEMS
AS_BASIC.Pred_decl (PRED_ITEM -> BASIC_ITEMS) -> PRED_ITEM -> BASIC_ITEMS
forall a b. (a -> b) -> a -> b
$ PropSL -> PRED_ITEM -> PRED_ITEM
prPredItem PropSL
pSL PRED_ITEM
pI
      AS_BASIC.Axiom_items aIS :: [Annoted FORMULA]
aIS -> [Annoted FORMULA] -> BASIC_ITEMS
AS_BASIC.Axiom_items ([Annoted FORMULA] -> BASIC_ITEMS)
-> [Annoted FORMULA] -> BASIC_ITEMS
forall a b. (a -> b) -> a -> b
$ (Annoted FORMULA -> [Annoted FORMULA])
-> [Annoted FORMULA] -> [Annoted FORMULA]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Annoted FORMULA -> [Annoted FORMULA]
mapH [Annoted FORMULA]
aIS
    where
      mapH :: AS_Anno.Annoted AS_BASIC.FORMULA
           -> [AS_Anno.Annoted AS_BASIC.FORMULA]
      mapH :: Annoted FORMULA -> [Annoted FORMULA]
mapH annoForm :: Annoted FORMULA
annoForm = let formP :: Maybe FORMULA
formP = PropSL -> FORMULA -> Maybe FORMULA
prFormulaM PropSL
pSL (FORMULA -> Maybe FORMULA) -> FORMULA -> Maybe FORMULA
forall a b. (a -> b) -> a -> b
$ Annoted FORMULA -> FORMULA
forall a. Annoted a -> a
AS_Anno.item Annoted FORMULA
annoForm in
                      case Maybe FORMULA
formP of
                        Nothing -> []
                        Just f :: FORMULA
f -> [ Annoted :: forall a. a -> Range -> [Annotation] -> [Annotation] -> Annoted a
AS_Anno.Annoted
                                   {
                                     item :: FORMULA
AS_Anno.item = FORMULA
f
                                   , opt_pos :: Range
AS_Anno.opt_pos = Annoted FORMULA -> Range
forall a. Annoted a -> Range
AS_Anno.opt_pos Annoted FORMULA
annoForm
                                   , l_annos :: [Annotation]
AS_Anno.l_annos = Annoted FORMULA -> [Annotation]
forall a. Annoted a -> [Annotation]
AS_Anno.l_annos Annoted FORMULA
annoForm
                                   , r_annos :: [Annotation]
AS_Anno.r_annos = Annoted FORMULA -> [Annotation]
forall a. Annoted a -> [Annotation]
AS_Anno.r_annos Annoted FORMULA
annoForm
                                   }
                                   ]

prBasicSpec :: PropSL -> AS_BASIC.BASIC_SPEC -> AS_BASIC.BASIC_SPEC
prBasicSpec :: PropSL -> BASIC_SPEC -> BASIC_SPEC
prBasicSpec pSL :: PropSL
pSL (AS_BASIC.Basic_spec bS :: [Annoted BASIC_ITEMS]
bS) =
    [Annoted BASIC_ITEMS] -> BASIC_SPEC
AS_BASIC.Basic_spec ([Annoted BASIC_ITEMS] -> BASIC_SPEC)
-> [Annoted BASIC_ITEMS] -> BASIC_SPEC
forall a b. (a -> b) -> a -> b
$ (Annoted BASIC_ITEMS -> Annoted BASIC_ITEMS)
-> [Annoted BASIC_ITEMS] -> [Annoted BASIC_ITEMS]
forall a b. (a -> b) -> [a] -> [b]
map Annoted BASIC_ITEMS -> Annoted BASIC_ITEMS
mapH [Annoted BASIC_ITEMS]
bS
    where
      mapH :: AS_Anno.Annoted AS_BASIC.BASIC_ITEMS
           -> AS_Anno.Annoted AS_BASIC.BASIC_ITEMS
      mapH :: Annoted BASIC_ITEMS -> Annoted BASIC_ITEMS
mapH aBI :: Annoted BASIC_ITEMS
aBI = Annoted :: forall a. a -> Range -> [Annotation] -> [Annotation] -> Annoted a
AS_Anno.Annoted
                 {
                   item :: BASIC_ITEMS
AS_Anno.item = PropSL -> BASIC_ITEMS -> BASIC_ITEMS
prBASIC_items PropSL
pSL (BASIC_ITEMS -> BASIC_ITEMS) -> BASIC_ITEMS -> BASIC_ITEMS
forall a b. (a -> b) -> a -> b
$ Annoted BASIC_ITEMS -> BASIC_ITEMS
forall a. Annoted a -> a
AS_Anno.item Annoted BASIC_ITEMS
aBI
                 , opt_pos :: Range
AS_Anno.opt_pos = Annoted BASIC_ITEMS -> Range
forall a. Annoted a -> Range
AS_Anno.opt_pos Annoted BASIC_ITEMS
aBI
                 , l_annos :: [Annotation]
AS_Anno.l_annos = Annoted BASIC_ITEMS -> [Annotation]
forall a. Annoted a -> [Annotation]
AS_Anno.l_annos Annoted BASIC_ITEMS
aBI
                 , r_annos :: [Annotation]
AS_Anno.r_annos = Annoted BASIC_ITEMS -> [Annotation]
forall a. Annoted a -> [Annotation]
AS_Anno.r_annos Annoted BASIC_ITEMS
aBI
                 }

checkHornPos :: AS_BASIC.FORMULA -> AS_BASIC.FORMULA -> Bool
checkHornPos :: FORMULA -> FORMULA -> Bool
checkHornPos fc :: FORMULA
fc fl :: FORMULA
fl =
    case FORMULA
fc of
      AS_BASIC.Conjunction _ _ -> (FORMULA -> Bool) -> [FORMULA] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all FORMULA -> Bool
isPosLiteral ([FORMULA] -> Bool) -> [FORMULA] -> Bool
forall a b. (a -> b) -> a -> b
$ FORMULA -> [FORMULA]
Tools.flatten FORMULA
fc
      _ -> Bool
False
    Bool -> Bool -> Bool
&&
    FORMULA -> Bool
isPosLiteral FORMULA
fl